upvote

points

by an0malous2 hours ago |
comments
upvoteby prof-dr-ir1 hours ago|
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

reply
upvoteby nperez192 hours ago|
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
reply
upvoteby nsingh21 hours 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.
reply
upvoteby thejokeisonme1 hours 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.
reply
upvoteby tmvphil1 hours 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.
reply
upvoteby macleginn1 hours 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.’
reply
upvoteby sebzim45001 hours 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)
reply
upvoteby 1 hours ago|
parent|
prev|
next
[-]
deleted
reply
upvoteby sigmar1 hours ago|
parent|
prev|
[-]
that paper isn't saying that. why are there so many single digit karma accounts misrepresenting that paper?
reply
upvoteby perching_aix57 minutes ago|
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.

reply