alt Hacker NewsThere's an entire paper claiming that many of these AI-generated Lean proofs are formulated incorrectly / mistranslated: https://arxiv.org/abs/2610.08144
Replies
sigmar • today at 9:17 PM
that paper isn't saying that. why are there so many single digit karma accounts misrepresenting that paper?
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.