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.