[CGamesPlay]

> I then gave both proofs to Opus and it confirmed their equivalence.

You could have just rubber-stamped it yourself, for all the mathematical rigor it holds. The devil is in the details, and the smallest problem unravels the whole proof.

[yosefk]

How dare you question the rigor of the venerable LLM peer review process! These are some of the most esteemed LLMs we are talking about here.

[falcor84]

It's about formalization in Lean, not peer review