Hacker News Reader

Math is a verifiable domain. Translate a proof into Lean and you can check it in a non-hallucination-vulnerable way.

But that's not what they're doing here. They're comparing Alphaevolve's outputs numerically against a scoring function

They did also take some of the informal proofs and formalized them using AlphaProof, emitting Lean.

Ah ok, I didn't notice that part, thx