tomkeen

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

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.