alt Hacker NewsNo it's already explicitly stated that translation to lean is a second step that happens after NL proof is done. That's why some of 400 paper dump is without lean proofs.
No it's already explicitly stated that translation to lean is a second step that happens after NL proof is done. That's why some of 400 paper dump is without lean proofs.
I wonder how are they sure the proof is correct before making a Lean translation. How is the work loop organised to force LLMs to reach a valid solution. I thought the ability to make it possible was the main advantage of using Lean.