Comment by mkarrmann

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

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.

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)

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

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.

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.

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.

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?