Hacker News Reader

Because the RLVR probably uses formalization to judge rollouts.

because LLMS are like drunk geniuses, without the rigor of lean they would drift into nonsense. Similar in chess they have 1700 ELO now but still some percent of their moves are illegal.

> All the major AI-generated proofs so far were done by AI without using lean

Is that true? I was under the impression they used lean as they went.

Yes that is the case. DeepMind's AlphaProof/Geometry that won IMO Silver used lean as an intrinsic part of the process 2 years ago, but things have shifted. When DeepMind and OpenAI won IMO Gold a year ago, it was solved end to end in language and translated to lean afterwards, and that has been the case since.

I stand corrected!