> The natural language proof was derived from the lean code, badly.
replyWas it? Are you claiming a LLM does reasoning in lean or what? Since this (and all the other proofs by OpenAI etc) have been in the reverse order [1]:
> The agents arrived at their resolution on Saturday, September 5, about 88 hours after the first agents were launched. Lean formalization and verification took an additional 17 hours via GPT‑6 Astra.
Yeah, I was surprised some people think LLMs are reasoning in Lean directly... all their training data is in NL.
replyIt's not that much of a stretch: give the LLM a top-level proposition for the thing you want to prove and have it hack away at it. Each sub-step is verified in lean so you know it's correct. But, the linked post definitely suggests otherwise.
replyThat is definitely interesting because how do you know the 88 hours of work are correct before you throw another 17 hours of lean formalization work on it? You could end up just finding out there was some hallucination in the original work.
An incredible number of people think that it is reasoning in lean. Argued with several people on this topic. I think they read headlines about lean being used by LLMs and assume it is being used to write the proof.
replydeleted
replyThat makes some sense. Given that the vast majority of math in its training data is going to be in NL/latex, I just assumed that the core reasoning happens in NL with occasional LEAN checks to ensure validity.
reply