Comment by yodsanklai

This is typical of working with agents, not only maths. "I implemented this with agent A, and don't understand the logic, but agent B think its correct". But then you ask a simple clarifying questions to B on a random thing in the code and it'll tell you that this part is actually wrong. At least in maths they have Lean...