3 ms·
Math is a verifiable domain. Translate a proof into Lean and you can check it in a non-hallucination-vulnerable way.
by khafra 11mo ago
Math is a verifiable domain. Translate a proof into Lean and you can check it in a non-hallucination-vulnerable way.
- griffzhowl 11mo agoBut that's not what they're doing here. They're comparing Alphaevolve's outputs numerically against a scoring function
- perching_aix 11mo agoThey did also take some of the informal proofs and formalized them using AlphaProof, emitting Lean.
- griffzhowl 11mo agoAh ok, I didn't notice that part, thx