The thing is that Navier-Stokes has a definition split off separate from the formalization, and that is what has been completed. People have looked at the definition of the final statement. This paper only mentions the proof and intermediate statement, not the final statement. The most likely case to me is that intermediate statements do not match, but the end result still holds.

Seems kinda odd then that it didn't occur to OpenAI to iterate until they reached a fixedpoint for both the informal & formal development b/c it's obvious that correspondence should have been part of their training pipeline.

Their aim was to create a correct-looking proof using as little resources as possible, not to create a correct proof.

Jesus Christ, so many people here who have no clue what they are talking about.

A proof of a theorem is different from the statement of the theorem. OpenAI has a Lean proof of the statement. That is all they need. There may be many different proofs of this statement, including NL proofs. It does not matter that these NL proofs may or may not be different from the Lean proof, at least for the correctness of the Lean proof. But of course the NL proof may be wrong. But who cares?

No. What the paper says is that in principle, translating NL statements to Lean statements is hard. Nobody doubts that, translating informal to formal text cannot be formally proven correct, so...

Does the paper give a single example of one of the OpenAI solved theorems with a Lean certificate where the Lean statement does not correspond to the actual statement from the mathematical literature? I don't think so, but in case I am wrong, feel free to provide that example.

This is explicit in the abstract:

> To demonstrate the effect of this result we provide several examples of AI mistranslations of NL statements and proofs into Lean in practice, resulting in mismatches between NL proofs and their Lean ‘verifications’. These include OpenAI’s announced Navier-Stokes proof.

Could /I/ be mistranslating the paper’s formal statement to NL? I don’t think so, but in case I am wrong, feel free to cite the correct formal statement that they claim as divergent between Lean and NL formulations by OAI.

[edit: typo]

Yes, you are misunderstanding what the paper claims. Navier Stokes for example is not such an example, only the proof is different. For their other examples, none of them they claim that they concern actually the open ai solved theorems. You are welcome.

you say that…

And yet I cited a specific statement made concerning N-S specifically, whereas all you’ve done is make patronizing remarks, and strawman arguments.

Have you actually read it? They give a handful of examples of mistranslations of both claims and proofs thereof, in relation to NS and Euler, though I do concede that they do not go as far as claiming outright the NS statement itself is mistranslated.

Unfortunately, lean proof alone is not enough. sidestepping the raging discussion regarding the meaning of mathematics, just because the lean compiles is not proof in itself that it is correct in the sense that mathematicians mean. Unless of course, you can prove that lean itself is correct, which you can’t.

we have seen “proofs” earlier this year that essentially abused some bugs in the kernel. it would be very convenient if every program written in rust was automatically correct if compiles - something i strongly suspect you believe - unfortunately, this is not the case for either.

Wow. You are exactly the person I am talking about in my original comment. Thank you for this illustration.

In case you are not aware, the actual theorem statement of N-S was never translated by an LLM, but was written independently by formal conjectures, as they say in the README [1].

A Lean proof has a much higher probability of being correct (in my opinion) than any published (either preprint or peer-reviewed) paper, yet no one before LLMs were walking around claiming every result published can't be trusted yet (without an actual reason).

We have seen one such instance of Lean bugs, which was found adversely against Lean (as in find bug then use this bug to prove Collatz, not just found when being asked to prove it).

It's also worth to note that the way N-S (and all the other proofs by OpenAI etc) have been found is first prove it in NL then translate to Lean. I.e. it would have to first believe it found a correct proof in NL, and then afterwards either accidentally or on purpose use a Lean kernel bug.

[1]: https://github.com/openai/NavierStokesAndEuler/blob/main/Com...

edit: Probably also worth to mention that the proof have been checked both by the Lean kernel and the independent nanoda kernel, so it would need to exploit bug(s) from both.

> A Lean proof has a much higher probability of being correct

Define “correct” in this context. That’s the real problem here.

Correct as in the Lean proof correctly finds a counterexample to N-S.

Here is what putting trust into a Lean proof means https://ammkrn.github.io/type_checking_in_lean4/trust/trust....

In particular the main ones are:

1. The theorem has been written correctly.

2. No exploit of a kernel soundness bug in Lean (and the independent kernel nanodo, which OpenAI also checks against).

In particular, if you trust this, then you don't need to care about anything else the Lean program does, no matter how many lines, lemmas etc. it makes along the way.

As I said above, the theorem statement have been written independently by formal conjectures, and you are free to read it yourself (or trust other people have done it).

So, assuming you don't disagree the theorem statement have been written correctly, you pretty much need to believe 2 is false, if you don't trust the proof [1]. And that's what I find has a rather low probability personally.

[1] As the book says, you also need to trust the hardware, firmware etc.

You may be overconfident here. The NL paper may be properly stating the Navier Stokes problem, and the Lean code may not be.

Here's from the paper--

3.1. When the NL paper declares stronger statements than what Lean proves

We commence with an example that complements those in §2. In the following example the AI autoformalisation results in a different Lean proof of a weaker statement.

None of the examples are of the NS lean statement. The validity of the latter is not under question ( in this paper ). Please note the distinction between “statement of NS” and “statement of lemmas used in the NL proof of NS”.

> the NL proof may be wrong. But who cares?

The people trying to understand the proof are probably following the natural language version. So they care.

I wouldn’t be surprised at all if that’s how this paper (which I did not read) arose.

Why would they do that, knowing that the one known to be correct is the Lean one? Just to claim that the (correct) Lean proof did not translate well to English? That would be weak, and a colossal waste of energy and time.

Why do people program in Python instead of writing machine code?

Why are review papers published? Executive summaries? "Introduction to X" books?

People's time and computational resources are finite. Summarising information -- ideally in structured ways that preserve important properties, but even in informal, unstructured ways -- is critical for making any kind of progress in this world.

It reminds me of how provably secure software was all the rage for awhile. Until people found that the idealized system/lemmas were so far from reality that the proved security was worse than meaningless because it gave a false sense of security.

In order to prove security, you must first simulate the universe.

> Who cares?

Everyone. I don't think many people working in fluid dynamics were surprised you can find a blow-up in Navier-Stokes. What would advance human knowledge is understanding the situations in which a blow-up might occur. In that context, the lean proof is necessary, but the non-lean proof is more important.

The statement written in Lean, is not actually a correct description of the Navier-Stokes problem. It's some other easier statement. That's why the Lean code may not be a proof.

Here's a quote from the paper. "In the following example the AI autoformalisation results in a different Lean proof of a weaker statement."

So the question is, was the Navier-Stokes problem framed properly in the lean code, or is some easier problem represented in the Lean code?

The "statements" here are statements of lemmas, not the statement of the main theorem. The main theorem statement was written by humans (prior to the OpenAI work), so there shouldn't be any concern that an AI mistranslated it.

That could be that these examples are lemmas, but in the introduction the authors conclude,

"In all cases the correctness of the formal proof does not say anything about the correctness of the NL proof."

The Clay Mathematics Institute has not yet accepted the proof as it takes a while to review.

"The Clay Mathematics Institute is dedicated to furthering the beauty, power and universality of mathematical thought. Curating the Millennium Prize Problems is one of the most important ways in which it pursues this goal. The rules governing the prizes describe the process for evaluating what has been achieved and for assigning credit. The process is deliberately unhurried, but we will provide updates."

https://www.claymath.org/news/navier-stokes-announcement/

We can see therefore that we don't know if the OpenAI program wrote the NL statement or proof correctly. Or if maybe it needs work. Or if maybe it has significant errors.

We also don't know if Astra properly wrote the initial statement of Navier-Stokes correctly in Lean.

My point is that Astra did not write the statement of Navier-Stokes in Lean, there was already a human-written statement, so there should be no concern that it has errors.

This article shows that we can't conclude from the working Lean proof that the NL proof is also correct, because they are different in some places. On the other hand I think it's unlikely that it's "very" broken. OpenAI first spent a lot of computer time to find the NL proof, and then less time to translate it into Lean. So if there were errors in the NL proof it seems they were not fatal, the agent translating it into Lean was able to patch them up as it went along.