The proofs may not yet be understood, but to claim they should not yet be accepted as solved is to claim there is a bug in Lean, which is a big claim.

▲

pfdietz a day ago | parent | next [-]

Plenty of these AI proofs have been accepted. On the most important result, on the Quasi-Riemann Hypothesis, there is no serious belief it's wrong. Mathematicians have already dissected and reformulated the claims.

The proof with the 11/12 constant, the simplest one, has already prompted what looks like chagrin from some. It's an unexpected combination of known results/techniques, a combination that apparently fell into a blind spot so it wasn't picked up before (even though it could have been, even 20 years ago).

I think these results are showing there was a lot of low hanging fruit that human mathematicians didn't have the breadth or mental bandwidth to find.

▲

ericpruitt a day ago | parent | prev | next [-]

Isn't it also possible that the written proofs themselves are incorrect, say, for example, by mis-specification of constraints? Let's say I publish what I claim is a proof that 2+2=4, but in the Lean specification, I proved 1+1=2.

	▲	thevinter a day ago \| parent \| next [-]
		To be pedantic, the proofs would be correct, they would just be proving the wrong thing. To address what you actually meant: it's possible but specifications are way easier to verify.
	▲	oulipo a day ago \| parent \| prev [-]
		The main issue would rather that the formalization itself has a bug, eg. those proofs that you're trying to formalize are not "1 + 1 = 2" but theorems which take already multiple pages just to enunciate. And in these enunciations (that are made by humans) there can be errors. In general, once the proof has been formalized, it's supposed to be the proof of the correct theorem (that's what the Lean proof-checker checks)

▲

pitchlatte a day ago | parent | prev | next [-]

the impression i get is that people don’t per se assert that exploitable bugs exist in Lean, but that the volume of (code) proofs published represent a new magnitude of challenge to the integrity of Lean.

the obverse would be to assert that Lean (or any other theorem prover) is infallible under all circumstances, present and future - an even weightier claim in my opinion.

▲

aktuel a day ago | parent | prev | next [-]

No. Lean being bug-free is a far bigger claim.

▲

ion_trapper a day ago | parent [-]

A bug which has allowed 700 proofs from diverse fields of math to appear as proven, and noone has figured it out yet?

	▲	afdbcreid a day ago \| parent [-]
		A single bug can usually allow you to prove anything you want. Saying that this is how the proofs were achieved is a totally different matter though, and probably incorrect.

▲

computerdork a day ago | parent | prev | next [-]

Hmm, am no expert at Lean, but on one hand, since it's a programming language, guessing it necessarily means like all other programming languages, it has bugs.

But on the other hand, agree with you that the chances that one its bugs causes a solved proofs to be wrong is probably very, very low. Yeah, each version of Lean obviously must be run against hundreds if not thousands tests of existing proofs to ensure it's working correctly...

... Although, one thing that is a little worrying is that some mathematicians have said the Lean code generated in these OpenAI proofs is supposedly really complex and undecipherable. It might be pushing Lean to corner cases that are not well tested.

▲

oulipo a day ago | parent [-]

It can possibly have bugs. That said, the "core" of Lean is a somewhat "simple" core that does simple things to check the proof, so it's quite rare to find meaningful bugs

▲

computerdork a day ago | parent [-]

don't disbelieve you, but just looked at the reference language, it seems pretty full featured as a programming language, even with basic classes, polymorphism, scope, namespaces... But maybe most of the mathematicians who actual code with stick with the simpler language features? And also, didn't look to deeply, these could be very simple features that actually aren't very sophisticated.

▲

oulipo a day ago | parent [-]

I mean Lean has two things: a full programming language, and proof checker. The programming language is used to create either code, or proofs. But the "created proofs" are using a very simple subset (a bit like an "assembly language"), and only need somewhat simple rules to be checked

So as long as the "somewhat simple" core that checks to proof is correct, it doesn't matter if the "programming language" has bugs: either in the end the "proof assembly code" generated by the program is right and is validated by the core, or it's not, and you need to revise your proof, or to check for either a bug in the programming language (it didn't generate the proof you were expecting), or in very rare case detect a bug in the simple "core"

	▲	computerdork a day ago \| parent [-]
		Ah, I see, that makes sense - and am guessing that most mathematicians (like most non-developers) who work with a programming language don't write "good" code and often ignore the organizational features like classes or namespaces. Yeah, could see how they really are just interested in the core feature-set of a programming language... although, have seen a bug in some high-usage low-level code before, which was greatly surprising. Still that was only one case in years of dev work.

▲

oulipo a day ago | parent | prev [-]

There's been many bugs found in Lean already, and there are probably still a few. So that's not the main issue.