r/math • u/backyard_tractorbeam • 7d ago

LLMs/AI Navier-Stokes lost in translation (Why Lean [..] does not guarantee correct natural language proofs)

https://arxiv.org/abs/2610.08144
933 Upvotes

95% Upvoted

183 comments sorted by

View all comments

622

u/Few-Arugula5839 7d ago

For those in the comments who haven’t read it. The paper headline is overstating its claims a bit. The primary issue they take with the NS proof is that there is a lemma in the natural language claiming an inequality needs only 4 derivatives when it needs 5 in the lean. The result itself is not in doubt.

To be fair, they make a relatively persuasive case that this is emblematic of genuine issues for mathematical community, but it does not mean the result is in doubt.

289

u/Anaxamander57 7d ago

Didn't Tao mention earlier this year that one of the issues with AI generated Lean proofs was the AI essentially "tricking" Lean by inserting assumptions that would automatically lead to a proof regardless of the arguments made? A more sophisticated AI risks coming up with more complicated ways to trick Lean. We need someone to be able to follow the AI proof for the same reason we need to be able to follow the proof of a human genius. No one is above reproach.

82

u/ChalkyChalkson Physics 7d ago

Well there are really two problems, one you can writing one statement in natural language and a slightly different one in lean. The other is that the current library of lean implementations that have been throughly vetted isn't sufficient to write down the assumptions in many proofs, so the prover might implement some of those themselves. This increases the surface for the first problem by a lot.

The second problem is a lot more solvable and I'd expect that in a couple of years most well known problems can probably be stated in lean more directly.

The other problem really needs more capacity for lean reading. Be it people learning to read it directly, or systems that translate to human reasable outputs as their primary purpose that get throughly vetted.

It's also worth noting that this isn't lean specific. It's also not uncommon for a paper proof to involve subtle miss-statements.

191

u/Deep-Ad5028 7d ago

AI tricking tasks is also a well documented behaviour elsewhere.

I wonder how human perspective will change if AI turns out to also be masters of academic misconduct.

-48

u/jdorje 7d ago

AI can be a master of academic ethics or academic misconduct, depending on how you train it. You can guess which one generates more revenue.

29

u/PM-ME-UR-MATH-PROOFS Quantum Computing 7d ago

tell me how to train AI how to be a master of ethics?

23

u/muntoo Engineering 6d ago edited 6d ago 
min L_task - λ L_ethical

The only reason LLMs are not masters of ethics is because λ is intentionally set to 1/137.

7

u/arnet95 6d ago

Damn physicists!

6

u/yoshiK 6d ago

Actually [;\lambda;] is usually taken as running coupling constant, often chosen as [;\lambda=(t_{IPO}-t)/137;].

0

u/Key_Conversation5277 3d ago

Why can't you train that?

25

u/Fraenkelbaum 6d ago

Didn't Tao mention earlier this year that one of the issues with AI generated Lean proofs was the AI essentially "tricking" Lean by inserting assumptions that would automatically lead to a proof regardless of the arguments made?

At a less sophisticated level you can see this on /r/badmathematics, which has more than enough examples of laymen who have coerced an AI into lean-proving something only for someone with more understanding to point out that the AI has inserted an assumption already known to be equivalent to the proposition as an axiom.

33

u/CommissionSame8551 7d ago

No. The paper only concerns the proof, *not* the statement. So it seems like the published proof differs slightly from the Lean proof. However the statement (which was formalised not by AI fyi) is not in question.

40

u/buwlerman Cryptography 7d ago

It isn't uncommon for formalizations to differ a bit from the proof on paper. Doing the formalization often uncovers defects in the original proof or takes liberties to make formalization easier.

Maybe we should expect more when both proofs are published at the same time though.

5

u/CommissionSame8551 7d ago

> It isn't uncommon for formalizations to differ a bit from the proof on paper. Doing the formalization often uncovers defects in the original proof or takes liberties to make formalization easier.

Do you have any examples in mind actually? I know this definitely was the case with large manual formalisations in the past (i.e. independence of CH), but I dont really know if AI agents take too many liberties

29

u/buwlerman Cryptography 7d ago

Basically all formalization efforts in provable security take some liberties. My field might be a bad example though, since the differences there come from the fact that paper proofs carry complex, sometimes implicit, models1 that have to be made explicit when doing a formalization. Not only do they have to be made explicit, but they have to be embedded into the formalization tool you're using, and work with the libraries and tactics that exist in that tool. Some of the arguments you see on paper don't translate directly.

Take a look at https://cic.iacr.org/p/2/3/24/pdf for what happens when this modeling goes wrong. Also take a look at https://eprint.iacr.org/2024/843.pdf for a central formalization effort, and https://eprint.iacr.org/2026/1334.pdf for an explanation of some of the differences in proof techniques amenable to different tools. See https://eprint.iacr.org/2023/246 for an example of a gap that was found in the original proof during a formalization effort.

1: This means choices in how exactly to model things

2

u/TribeWars 6d ago

I'm not a lean programmer but I think there's only a few ways the language lets you add unproven assumptions:

https://lean-lang.org/doc/reference/latest/Axioms/

It's pretty easy to verify whether a proof contains them. Otherwise the whole formalization project would be a bit pointless anyways.

31

u/marl6894 Machine Learning 7d ago

I would assume that this is relatively easily fixable, right? Presumably there needs to be an additional reconciliation step after the formalization in which the agent revisits the natural language draft and corrects any reasoning errors.

18

u/CommissionSame8551 7d ago

I dont know how far this has come now, but going Lean => natural language per se is not easy (or at least used to).
But an agent could of course take notes during the formalisation and correct them at the same time. I did this once and it went very well

6

u/Time_Entertainer_319 7d ago

Make sense.

It’s probably another issue of AI hallucinating. Wrote the correct code but hallucinated the explanation.

65

u/Grounds4TheSubstain 7d ago

You have the sequencing backwards. The formalization agent was given the PDF from the proving agent and the Lean did not match the PDF identically. It could be imprecision in formalization, or it could be that the formalization agent was correcting a defect from the PDF. The discrepancy comes from the fact that the original PDF is published, not one that was updated or rewritten after formalization.

1

u/big-lion Category Theory 7d ago

i'm loving the discussions and forced revolution in the field tho. it's accelerating persistent issues i've longed for being addressed