Hacker News Reader

Comment by JonChesterfield | Hacker News Reader

> Autoformalization has become a practical reality in 2026

Uh, _maybe_. I've been translating papers into lean for the last week and the correlation between the formalized result and the papers is extremely poor. The cycle seems to be "have a go at the paper, it's a bit hard, prove something different, proclaim success". It's still faster than doing it all by hand but paper in -> lean out in no way ensures a correspondence between the two.

View on HN

I've formalised a few dozen papers from 80s-90s with lean and holy cow the number of author's typos and straight up errors and sometimes false statements is pretty scary. The solution path may not be the one indicated or used by the author, but at least you can easily spot all those issues which would have been very hard to do by hand

> prove something different

I'm not sure but do you mean "prove the final end result using a [¿slightly?] different path"?

No, prove something else could mean proving something very trivial thus making the proof meaningless on its own.

IE a proof can be true, rigorous, and not at all what was asked for.

It's possible, but less likely when the problem definition is coming from a common library rather than being redefined for any particular proof.

Think of it this way. A math paper is pseudocode that has never been run. A Lean formalization is a running program. (It really is.)

In the process of formalizing, you find bugs, you find gaps, you find ways to fill those in. Maybe you rewrite part of the proof. Maybe you didn't quite wind up with the same result. Perhaps your theorem has some new conditions or something.

Was the original paper true? Maybe. But that isn't what you verified. What you verified is almost surely true though. So you take the win, and move on.

They mean a different statement, a different theorem. You have to understand that translating a theorem written in English text to lean code is also a non trivial step.

When independent reviewers compared the paper's text to the generated Lean formalization, they found that whenever the AI hit a wall, it quietly altered the statement like bumping a bound requiring 4 orders of derivatives up to 5 orders, or shifting sign indices (+1 vs -1) so the proof checker would accept the code.

The Lean kernel did its job verifying that the compiled code was logically consistent, but the code wasn't proving what the English paper claimed.

Could you be more specific? I think proving the right thing is the one serious weak spot of the recent deluge of AI-proven results (much more serious than soundness bugs in proof checkers -- these can be fixed and the checks rerun).

The paper is "Navier–Stokes lost in translation" by Bastounis, Circelli, and Hansen (Cambridge/DAMTP): https://arxiv.org/abs/2610.08144

If I understood that paper right, what it claims isn't quite the bombshell that it initially looks like. (Though it is still startling.)

I think they are saying: when OpenAI put out their paper purporting to prove that Navier-Stokes with smooth forcing can blow up, along with something purporting to be a Lean formalization of that paper, (1) the Lean formalization really is a proof that Navier-Stokes with smooth forcing can blow up (so they genuinely did prove the thing that the Clay Institute wanted them to prove), but (2) the Lean formalization doesn't perfectly match the paper. I think the jury is still out on whether the paper itself is also a valid proof of the result, even if not quite the same proof as is in their Lean formalization.

I'm a bit surprised that the workflow for AI theorem-proving hasn't turned out to be a sort of interleaving of natural-language theorem proving and Lean formalization. That seems like it could work better and leave less room for this sort of gap between "kinda human-comprehensible writeup, may or may not actually be a proof" and "incomprehensible Lean formalization, definitely a proof of something, may or may not have much to do with the natural-language writeup". Instead, what seems to happen is that they set the robots loose on writing a natural-language proof, and then (sometimes) also get them to produce a Lean formalization of what they've done.

Thanks, that was exactly my understanding of it too (based only on HN comments I've read about the paper).

Reply on news.ycombinator.com