News for hackers. Stuff that matters.

A comment on I struggle to believe that AI R&D is ingenious. Parent comment

Re:I struggle to believe that AI R&D is ingenious by ogogmad on Friday November 06, 2026 @04:51AM (#50390318)
In my experience they write an informal proof first, check it without Lean, and only then turn it into Lean code. What they're truly bad at is explaining their proofs. Until they improve at that, we'll have to keep asking Lean whether they solved something correctly.

While they're not great at explaining their own proofs, some models are good at explaining older, human-written proofs.

[ Parent | on HN ]
Re:I struggle to believe that AI R&D is ingenious by ccppurcell on Saturday November 07, 2026 @08:13AM (#50404295)
I definitely don't know but I got the impression it's the opposite. Based on the observations about Navier Stokes and the natural language proof not matching up with the lean proof and other things. They generate lean and convert it into natural language at the end. But really I could be wrong just giving anyone interested a lead to check out.
[ Parent | on HN ]