Hacker News Reader

Comment by nayroclade | Hacker News Reader

So, the AI wrote a NL proof of Navier-Stokes, then incorrectly auto-formalised it to Lean, but still ended up with a verifiable proof of Navier-Stokes? That seems... strange?

View on HN

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.

The OpenAI announcement says

> 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.

This seems pretty clear that they found the proof first and then mechanized it afterwards.

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)

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.

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.

The mental gymnastics on display is amazing to see. You clearly have no idea of what you are talking about.

I don’t. But I do know how the scientific method works, and OpenAI’s display is anything but. Until what they have demonstrated is reproduced I take their claims to be nothing but marketing. A for profit company will lie in order to maximize their profits. Above I presented an alternative hypothesis, which is probably wrong, but until OpenAI’s results are replicated I will believe my alternative hypothesis just as much as I believes the claims of the for profit company making them.

I’m a non-math layman, and not a scientific method knower like yourself. How does one usually “replicate” a math or Lean proof?

Hopefully not in the same way you should never naively trust compilers!

The generation of the proof can be replicated. And if it can‘t we should be suspicious of their claims.

It's the method they used to create the proof that's in question here. They claim their amazing product did it, and therefore you should buy their product because will do amazing things for you too!

> I presented an alternative hypothesis, which is probably wrong, but until OpenAI’s results are replicated I will believe my alternative hypothesis

If you think it's probably wrong, why believe it?

In the absence of evidence, a guess is the best you got.

And, no until OpenAI’s results have been replicated, I don‘t believe companies own words about their own products, and therefor a marketing statement is not evidence.

Not necessarily monkeys but thinking in Lean first is quite plausible

You can't consider them monkeys if you need 1000 of them instead of 2^1000.

Reply on news.ycombinator.com