auggierose

> We rebuild what was. You walk through it.

Closing the page right there.

Again, you don't need to check the proof, Lean does that. You need to check the statement, which is a much easier task. So yes, you are wrong. Skepticism is good, but it is usually just ignorance.

They tried that with Navier-Stokes. Didn't really work out.

A correct solution verified in Lean will count in perpetuum. It is fine if you want more, but an achievement is an achievement, even if it is by AI.

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

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.

Yes, Grant Sanderson might be a great example. I am not doubting the competence of the "good lecturers" I was referring to. But that is different from being able to introduce the big new concepts that give the big new results.

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.

You can get the opposite extreme quite often as well, I'd think. How many really good lecturers have never proven a new important result?

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?

Yes. I don’t have a solution for this, but that is what it is.

What I am seeing is not people not being diligent in their research, but people not being diligent in their reviewing of research. But maybe there is a positive feedback loop here...

Yes. If not, we will be starting to chop off heads.

All of these things are definitely not necessary to know about to successfully use Lean, and not even useful to know for proving things in Lean.