> The natural language proof was derived from the lean code, badly.
Was 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.
Was 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.
[1]: https://openai.com/index/navier-stokes-solution/