bckgrndrdtn

> These proof checkers all have bugs, every single one

Please show me a proof of `False` in Lean.

It's a mixed bag. Some people don't use AI, for the usual reasons that people don't use AI. Others have used AI to write Lean programs. For example the 200K loc example mentioned in OP. But generally speaking, the quality isn't good enough yet. And when you've looked at 13 AI-generated examples and found them lacking on various axes compared to Mathlib, then you'll take a break before being motivated to look at example 14.

You are conflating:

(i) accepting that a piece of code is a valid Lean proof (ii) merging a valid Lean proof into Mathlib.

Valid Lean proofs need maintenance. Mathlib is a living blob of code. People care about how fast the proofs typecheck. Many other properties of code play a role.

Not everything that is true is worthy of immediately including in the Encyclopaedia Brittanica.

You would think that the people maintaining Mathlib are a subset of {understands type theory and how theorem provers work}...

Yet they don't merge this stuff, for many different reasons, including that those 200K lines are free as in puppies.

You can have all the type theory of the world, but the library still needs maintenance.

Change a simp-lemma in a file close to the root. Oooh noes, now there's 987 errors in the 200K loc that we merged last week. And there's nobody there who understands how to fix them.

Just use AI to fix. Or maybe just don't merge the code and let it sit in a downstream library?

And wait until there's evidence that the code is stable, high-quality, with well-designed APIs. And then decide that it might be worthy including in a more foundational library.

All well and good, but we should also admit that under this criterion 95% of published math papers don't contain new ideas but are just filling in stuff that previous authors missed.

The future is now. See the article under discussion for some examples.