Hi! One of the authors here. Whether checking the LLM-generated Lean statements/definitions is easy or not depends heavily on the area of mathematics and the concrete definitions at play. In this case it was remarkably easy. As you can see in the repository, the definition of a countermodel is easy to parse, and the statement corresponding to their nonexistence for n <= 11 is also very easy to check. If you have any questions regarding them, I would be happy to answer them.

Personally, this is one of the cases with LLM-generated Lean that I feel most comfortable with: the proofs are all mathematically simple, and we included an example of correctness for one of the SAT constraints in the paper to show that there is nothing complicated about them. Writing them all in Lean, however, would be a very tedious task for which I see no particular benefit (i.e., it's not like some other formalization projects in which one learns something by formalizing; for an example of a human-written Lean correctness proof of a SAT encoding, you can check the paper https://arxiv.org/abs/2403.17370 in which I participated).

Regarding the byte-for-byte equality, the point is that we first had the Python code (which we wrote manually), and then asked LLMs to implement an encoder in Lean that would not only produce "equivalent" formulas but exactly equal formulas, meaning that it would use the same variable indices and the same clauses in the same order. It is well-known that such superficial factors (e.g., clause or variable ordering) can actually have large effects on solver performance (see https://www.cs.utexas.edu/~marijn/publications/pos18.pdf). The Python code is not part of the trust chain, and the Lean code does not rely on it in any way. We included the Python code in the repository since it's much shorter and easier to read.

> This is extremely unconvincing. Manual review of 10,000 lines of AI generated code is a terrifying prospect.

With https://en.wikipedia.org/wiki/Lean_(proof_assistant) (and other proof assistants), you need to review only the lines that correspond to the theorem that you want to prove and their types (I am not very experienced when it comes to lean, but I would assume that comes down to a few hundred lines of code, at most). The rest is left to typechecking (which, I would expect many in the field to agree, is at as reliable than your average peer review process in professional mathematics, and likely much more). That's the reason why Lean4 is making such a fuzz now.

That itself is not trivial too, but way easier than reviewing every function and definition used to prove that the theorems have indeed the types they claim.

If one accepts the proof of the https://en.wikipedia.org/wiki/Four_color_theorem, then there should not be new reservations these proofs; except from the maybe new additional failure scenario that the authors (still correctly!) proved theorems that don't state what they think they stated.

To sum it up: There is IMO no domain more suited for using LLMs than mathematical proofs that can be formalized using Lean4. The fact the hype-circle started earlier in software than in maths is due to the difference in monetary incentives I would assume. (Or another, rather radical and not really serious phrasing: "When it comes to Lean4 proofs that typechecks, there is no AI slop" - the theorem being proven might be uninteresting, but the proof itself is very very very very likely to be correct)

> “byte-for-byte equal”

The term itself or its association with LLMs? I would get the latter, if its the former: It's an desirable property to have, I always like seeing people going that far (assuming obviously that they indeed did so, and in the places where it matters!)