> But it also appears that no human has understood just about any of these proofs yet

Has anyone verified any of the proofs produced by OpenAI or is everyone just assuming that it just be true because the Lean code checks out? Couldn’t the Lean code just be formulated incorrectly?

▲

prof-dr-ir an hour ago | parent | next [-]

It's a mixed bag I think.

For example, the statement of e.g. Fermat's last theorem in Lean should be understandable to anyone who played The Natural Number Game [0] and knows a bit of mathematics and programming. For the proof, you trust the compiler.

The statement of other theorems can be much more delicate, and the Lean formalization may require an extensive introductory section which will need to be carefully checked.

Then there are the cases where no Lean formalization is currently available, and all we have right now is an often impenetrable pdf in the OpenAI repo. I would not at all be surprised if some of those contained logical gaps.

Time will surely tell, but there are certainly doubts and lots people are very busy checking these results.

[0] https://adam.math.hhu.de/#/g/leanprover-community/nng4

▲

nperez19 2 hours ago | parent | prev | next [-]

There's an entire paper claiming that many of these AI-generated Lean proofs are formulated incorrectly / mistranslated: https://arxiv.org/abs/2610.08144

▲

nsingh2 an hour ago | parent | next [-]

Note that paper is saying that the lean proof and the natural language proof do not necessarily coincide. It is not saying that the lean proof is wrong, just that the lean proof does not necessarily mean the natural language proof is correct.

▲

thejokeisonme an hour ago | parent | next [-]

A lean proof and a paper proof can diverge. But the statements have to correspond. I think that is what "mistranslated" means here.

	▲	tmvphil an hour ago \| parent [-]
		But the "mistranslation" is of the procedure that arrives at the final statement. The final statement, the thing that the lean code proves, itself has been well vetted by humans. So the lean proof correctly proves the NS blowup, it's just that the natural language paper has some mistakes and doesn't exactly follow the route the lean proof takes.

▲

macleginn an hour ago | parent | prev [-]

The thing is, you often see people saying, ‘They have a Lean cert, so it has to be correct, even if I don't understand it.’

	▲	sebzim4500 an hour ago \| parent [-]
		They are right? The lean proof is correct. It's the natural language proof that potentially isn't (or at least it isn't identically structured to the lean proof)

▲

sigmar an hour ago | parent | prev | next [-]

that paper isn't saying that. why are there so many single digit karma accounts misrepresenting that paper?

▲

an hour ago | parent | prev [-]

[deleted]

▲

perching_aix 42 minutes ago | parent | prev [-]

> Couldn’t the Lean code just be formulated incorrectly?

I believe so, even with all the usual safeguards properly in place: https://news.ycombinator.com/item?id=49672339

> is everyone just assuming that it just be true because the Lean code checks out?

Kinda? It's only been 24 hours since they dumped 722 manuscripts on the world, most of which are apparently basically unreadable, and only some of which come with a Lean proof, which in itself is not a joy to read afaik.