Note that paper is saying that the lean proof and the natural language proof do not necessarily coincide. It is not saying that the lean proof is wrong, just that the lean proof does not necessarily mean the natural language proof is correct.

▲

thejokeisonme a day ago | parent | next [-]

A lean proof and a paper proof can diverge. But the statements have to correspond. I think that is what "mistranslated" means here.

▲

tmvphil a day ago | parent [-]

But the "mistranslation" is of the procedure that arrives at the final statement. The final statement, the thing that the lean code proves, itself has been well vetted by humans. So the lean proof correctly proves the NS blowup, it's just that the natural language paper has some mistakes and doesn't exactly follow the route the lean proof takes.

	▲	thejokeisonme 19 hours ago \| parent [-]
		No, this isn't what this is about. From the abstract: > In this process, an AI system translates the text from a natural language (NL) into a formal language such as Lean. Once this translation is done, the argument expressed in the formal language can easily be mechanically verified. The purpose of this article is to demonstrate why this process may offer no confidence in the original NL argument, owing to the various difficulties in performing the translation semantically faithfully.

▲

macleginn a day ago | parent | prev [-]

The thing is, you often see people saying, ‘They have a Lean cert, so it has to be correct, even if I don't understand it.’

▲

sebzim4500 a day ago | parent [-]

They are right? The lean proof is correct. It's the natural language proof that potentially isn't (or at least it isn't identically structured to the lean proof)

	▲	macleginn 17 hours ago \| parent [-]
		By "it" people in such cases are usually referring to the NL proof. It seems nobody has any hope of undersanding AI-generated Lean code any more, if only due to volume.