Really interesting how they let agents write free-form text first(in what he describes as university exam level verbosity style), not Lean, and then at the end, when the agents claim to have found the proof, have other agents convert it to Lean and verify the proof there.
2 comments
[ 2.6 ms ] story [ 12.5 ms ] threadReally interesting how they let agents write free-form text first(in what he describes as university exam level verbosity style), not Lean, and then at the end, when the agents claim to have found the proof, have other agents convert it to Lean and verify the proof there.