Post #3992424

OK, so this article is discussing followup work to the recent work on the Erdős unit distance problem. It says: “The basic structure of the proof is that a profound theorem in number theory due to Golod and Shafarevich from the 1960s could be used to construct a counterexample to the conjecture.” OK so far. Later it continues: “Boris Alexeev announced on the Lean Zulip that he had steered ChatGPT to a complete formalization of the Erdős counterexample, assuming nothing beyond the axioms of mathematics. … [The model] had generated 1.2 million lines of Lean code in the three weeks that it had worked on the project. … One cannot trust AI-generated code so I ran it in a sandbox on my machine … . Wow.” I understand that the Lean code can be easily checked for correctness by the Lean kernel, I think that part is clear. But who is it exactly that is looking at 1.2 million lines of autogenerated Lean code to confirm that the claim that has been formalized and checked actually says what was wanted? For example, won't it start with a huge pile of Lean formalizations of concepts from algebraic number theory? Mathematicians don't always understand one anothers' definitions, isn't it possible that one of the Lean definitions is subtly different from what is really needed, so that the theorem that has been checked isn't saying what we thought it was? In what way is 1.2 million lines of autogenerated and auto-checked Lean code useful for anything? This is a serious question. I don't understand. https://xenaproject.wordpress.com/2026/07/20/human-mathematicians-are-being-outcounterexampled/