This same thing happened back in the 10 advances in math and CS release a month or two ago. The non sofic group construction relied on false prior literature. They realized this and fixed it in the lean program but didn't modify it in the writeup, so the written proof was both incorrect as stated and did not correspond to the lean proof. I was surprised how little press it got at the time, it seems like a huge risk factor.

Or the AI wrote a NL proof of Navier-Stokes, began rewrite in Lean, then discovered a false / handwavy / easier to write in Lean / etc approach of some parts of the proof, and modified it accordingly. Since there wasn't any backpass from Lean to NL to include any changes it did due to any of the above reasons, the proofs aren't identical. That's what I think is most likely.

If the reason for the differences was done intentionally in Lean (as opposed to hallucinate e.g. m+4 vs m+5 as mentioned in remark 3.2), then a simple recording of differences, and then afterwards pass back any changes to the original NL would fix the issue. If it was hallucinated, then there is no guarantee it wouldn't keep hallucinating, and thus you might never end up with the same proof no matter how many passes you do back and forth (see remark 3.4).

I don't know if we can really be clear about the order of things, but I think even without AI maths is filled with "someone provides a proof of X, and the proof itself is wrong/incomplete but X itself is true".

"Incomplete" proofs might be a way of viewing this. You have a NL argument to prove X. It turns out the NL proof has holes you can drive a truck through. So... you go around and patch the holes.

The resulting proof is different! You can start off with a bad proof and find a correct proof. Sometimes.

EDIT: for French speakers (maybe autodub gets you there) I saw a very nice simple case of this recently. A commonly stated proof for a relatively simple theory. The proof has a giant hole in it, and completing it requires some work [0])

[0] https://www.youtube.com/watch?v=kQBu6NH1u3I

This happens all the time with human researchers.

e.g. one of the lemmas in the NL description is false, but a weaker version of the lemma (that does hold) is sufficient for the proof, so the (incorrect) lemma is never formalized.

It's not actually the same model that solved the problem that did the translation. Astra did the translation after the intenral model produced the NL Proof. As for the discrepancies, It's not necessarily right to think of this as 'incorrect formalisation'. Maybe it was essentially a 'proof refactoring'. Maybe Astra thought some parts could be easier expressed in a certain way, or maybe aspects of the NL proof were kind of handwavey etc.

Why do you assume this order? I would assume the AI starts with lean (that's what it was RL'd on at least) then tried to translate the proof for us humans, which is quite hard.

I'm not sure about it but it seems plausible given the potential error.

Edit: they explicite say that your order is correct in the post

I would expect it's the other way around. The AI wrote a Proof of NS in lean and write up a NL proof based on the lean one. The authors claim that openAI did NL -> Lean, but that is unsubstantiated.

Proof steps can become different in Lean but still work to prove the theorem. Incorrect proof steps in the NL paper could also be converted to correct ones in Lean. The paper shows some examples of this. So the NL paper can't be trusted even if Lean verification passes, but it doesn't immediately mean that the NL proof is wrong or that Lean is checking the wrong thing.

Trying to map this observation to code and appreciate them starting with very simple examples (that Astra screw-fixed into lean.) But in a simplified way this is close to promting the model to create a set with the members 1,2,1,5 and it correctly creates {1,2,5} in code. So The initial "proof" / instruction was wrong and it silently fixed that. ( Which is one of the failure modes they're describing)

it's the result of thinking carefully about the translation process.

humans as a whole have always known the weakness of natural language is in its precision. In a way this isn't strange that this issue has come up.

If you’ve tried any formalizing in codex Astra often works solely in Lean

Or maybe the AI didn’t write Lean proof at all, or rather, not the LLM at least. But instead OpenAI has an internal traditional reinforcement model that is able to stumble on the Lean proof by the share amount of compute power available to them thousand monkeys on a thousand typewriter style. And then pretend LLM did it because that is what they are selling.

Well the theorum statement (what it proves) is short and easy to verify. I would not be surprised if hundreds of mathematicians have looked at it at this point.

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.

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, it's the Lean proof that's correct, it's the natural language one that has the error.

To put it in code terms.

1) The code and the comments disagree.

2) The code passes the tests.

3) The comments promise functionality the code does not implement.

The first post was "It doesn't meet the business requirements the comments indicated, so the software is broken." The replying post was "Actually, the business requirements were faithfully turned into tests, so the software is fine. The comments need to be rewritten"

Also an outsider to the field and wondering the same thing. I can't see the difference. Can someone explain please?

The English language description doesn't do the same thing as the code the AI wrote.

and clearly the computer science perspective is: get rid of the humans and express everything directly in lean so the computers can keep getting work done!

;)

This is the formalization that was proven in Lean. As of now at least, it's believed to be a correct statement of the problem.

https://github.com/google-deepmind/formal-conjectures/blob/8...

Nobody is claiming they've misformalized Navier-Stokes.

>or if the initial statement in Lean is correct. I suppose that's obvious.

Is it obvious? The formal statement that Astra proved was written by a human, submitted to a DeepMind repository, and reviewed by human experts in a pull request. It's completely independent of OpenAI's effort. No expert in PDEs or formal verification has disputed it as far as I'm aware.

https://github.com/google-deepmind/formal-conjectures/blob/8...

I was having trouble wrapping my head around it but this cleared it up.

> The natural language proof was derived from the lean code, badly.

Was it? Are you claiming a LLM does reasoning in lean or what? Since this (and all the other proofs by OpenAI etc) have been in the reverse order [1]:

> The agents arrived at their resolution on Saturday, September 5, about 88 hours after the first agents were launched. Lean formalization and verification took an additional 17 hours via GPT‑6 Astra.

[1]: https://openai.com/index/navier-stokes-solution/

That makes some sense. Given that the vast majority of math in its training data is going to be in NL/latex, I just assumed that the core reasoning happens in NL with occasional LEAN checks to ensure validity.

They do not. Maybe if they take Lean classes? Maybe starting this year they will but my youngest kid is on their like 5th math class in undergrad and hasn't had any lean at all. Not all undergrad math majors even take PDEs; applied maybe, unless you are doing applied discrete math (graphs, combinatorics).

Not a mathematician, but "pretty sure" might not be good enough to resolve this question.

The same JavaScript code compiles to different machine representations under different browser engines; yet webdevelopers don't need to learn assembly.

There is an abstract javascript machine which can obviously be translated to hardware instructions. "Obvious" in the mathematical research sense, as in the statement is flat out wrong under closer inspection. Websites regularly crash under memory pressure.

But they are good enough most of the time, and that's the key. With more resource a more correct program can be created, but cost-benefit calculations show a ceiling. A local pet store does not have the money to pay 2000 hours of formal verification work, and usually a WordPress site is good enough.

Mathematicians work with their brains. They have finite time to understand papers. Formalists say that all theorems could be reduced to logical axioms, but most of time it's jumping at a much higher level, because no one has time for minute details. Proofs are theoretically right or wrong, but in practice there are "slightly wrong" proofs, where there are some minute errors that "feels" like can be correcte, and most of the time it can be. This ambiguity is not a problem, but a feature of mathematics, because it means more time can be spent to move faster at a higher level of abstraction, but this would be lost with Lean.

There are bugs found in programming language implementations all the time. I guess you are switching to machine code, good luck.

Is not a natural language (NL) proof a demonstration of mastery and understanding?

If you understand the Lean, then you can create a NL proof. The LLM clearly doesn't understand the Lean code it produced.

>the statement proven is not the conjecture for which proof is required for the problem to be considered "solved".

that's not the claim. the formal statement of the problem for the NS proof was written by humans not autoformalized.

That's not the claim made in TFA. See the sibling comments, in particular about the DeepMind formalization.

Please make your substantive points without swipes. This is in the site guidelines: https://news.ycombinator.com/newsguidelines.html.

Does that contradict what I said? In that quote, it says that the NL proof does not correspond to the Lean proof. However, the statement of the theorem in Lean is independent from the NL proof. It comes from a DeepMind repository, which as far as I'm aware has been accepted by the community as a valid formalization of the original Clay Institute statement.

https://github.com/google-deepmind/formal-conjectures/blob/8...

Both proofs may be correct, and the problem may indeed be solved. My point is that it should not be assumed.

> Maybe read the original article before replying, at a minimum.

Maybe read the comment before replying, at a minimum.

I would say it's released in the spirit of open source. "Peer review" in the narrow sense exists primarily to assign prestige in academia; but there's nothing stopping anyone from "peer reviewing" the GitHub repository.

not submitting to whatever journal is quite different than saying they are "beyond peer review"

are people not reviewing openai claims right now?

Because they want to release everything on github so everyone can peer review it themselves

This is far more efficient and they’re telling the academic industry to grow up

Sister comments are saying that academics dont like the Lean programming language and see a lack of human language described proof. Doesn’t sound like something I should care about but I’m watching for a better human language description of the problem as this discussion evolves

You are confusing two levels of indirection here.

Peer review is a proxy for correctness.

Peer review journal is a proxy for quality peer review, or at least it was, once upon a time.

"not interested in" != "beyond"

This. The proof of Fermat’s Last Theorem took 15+ months to check. It’s absurd to see the media reporting that these big problems are solved based off of a news release and a hastily and mostly AI-written manuscript, and OpenAI et al. are all too happy to run with said breathless reporting.

there's breathless reporting of just about everything scientific. physics, astronomy, archaeology, etc. have this sort of thing all the time.

yet i have never seen anyone say "the idea that physicists are beyond peer review is harmful" because some mainstream news articles published a piece about dark energy or whatever.

Exactly. Coverage here is "OpenAI has solved problem X", not "OpenAI has claimed to solve problem X."

I was pointing out that your original comment (before you edited it to just say "ok") did not properly represent the claims of this paper.

I am not making any claims about mathematicians as a collective group, because mathematicians have many diverse views on AI and can't be lumped together into a single "they" (as your comment seems to imply that they can). In fact, some academic mathematicians even work for the AI companies. Your comment seems to imply that if a group of mathematicians publish some statement, then that statement must speak for all mathematicians, but that's simply not true.

If you're responding to the parent post, as most of us are, the Lean proof is not irrelevant.