First up: thanks for your hard work here in the sneer mines during these ridiculous times!
I saw this being ignored on HN and I thought that you might appreciate it:
NAVIER–STOKES LOST IN TRANSLATION – WHY LEAN VERIFICATION OF AI AUTOFORMALISATION DOES NOT GUARANTEE
CORRECT NATURAL LANGUAGE PROOFS
arxiv.org/pdf/2610.08144
(Apologies for shouting!)
The authors (who don’t seem to have a problem with LLMs) point out that automatic translation of natural language mathematics into Lean is very hard, actually. They also highlight some examples of such translation errors in the Navier-Stokes “paper” published by OpenAI. They tread lightly and don’t take a position on the correctness of the proof.
I also thought the reference to the Solvability Complexity Index (which is new to me) was interesting, and there’s an appendix with an explainer on how the SCI hierarchy is constructed. According to this scheme, autotranslation of natural language proofs is strictly harder than the Halting Problem.
This is all beyond my level, but I’d love to see what our local experts think of it.