Are We Stuck with Lean?

Metamath contributor here! Each proving tool has its pros and cons, but always happy to see Metamath noted :-).

One thing that's cool about Metamath is that the axioms are not built-in. It's true that the most-used system is based on classical logic and ZFC set theory https://us.metamath.org/mpeuni/mmset.html ... but you don't have to use that system. There's a well-maintained database using intuitionistic logic: https://us.metamath.org/ileuni/mmil.html ; on the so-called "New Foundations" (a many-sorted system): https://us.metamath.org/nfeuni/mmnf.html ; on HOL https://us.metamath.org/holuni/mmhol.html ; and you can make your own if you want to.

In Metamath the proofs hide absolutely nothing. There's no hand-waving "it's obvious that". Every step in a proof must be rigorously and directly proven by some axiom or a previously-proven theorem with absolutely no exceptions. This also means that while finding proofs can be hard, verifying proofs is fast. I just ran a proof verification run of over 47,000 theorems in 6.35 seconds. In the Metamath Proof Explorer / set.mm database (the one with classical logic and ZFC), we routinely run multiple provers by different people on every proposed change. So not only is the kernel small, it's implemented by multiple different programs, making it extremely unlikely we'll accept an invalid proof.

This video I made years ago summarizes Metamath: https://www.youtube.com/watch?v=8WH4Rd4UKGE

I find it really strange that people who don't use lean don't just get on and use the alternatives rather that trying to get everyone who is using lean to use something else. It feels exactly like if all the emacs users in the world tried to force all vim users to use emacs.

It's important to meet reality head on: Every mathematician is not going to collaborate on the same tooling (as wonderful as that might seem on the surface to be as an outcome) human beings are different and want different things, and people are productive in different environments. In particular, people who want to formalize results within the standard framework (including zfc) are never really as a group going to care that much that lean4 doesn't let them formalize results outside of zfc.

I don't see what the issue is. Isn't the entire point of LLMs that we can easily translate between languages? What better way to cross check the correctness of a proof than to run it on several different systems simultaneously.

Metamath's Python verifier - its trusted kernel - is just 700 lines of Python short: https://github.com/david-a-wheeler/mmverify.py/blob/master/m...

Metamath Zero's Haskell implementation 700, and the C implementation 1000 lines (or 1800 overall) https://github.com/digama0/mm0

How do other proof systems compare?

Some bug counts: https://tristan.st/blog/in_search_of_falsehood

https://github.com/Syzygies/Compare

I spent far too long comparing dozens of languages, only some of which are part of the above project, before switching from Haskell to Lean for a new phase of my math research. Lean wins for me without considering or using dependent types (for now). It is simply a better programming language than any I have seen.

This is a critical advantage for those interested in proof. One codes tactics using the same language as for proof.

https://github.com/Syzygies/Compare/blob/main/source/lean/Na...

I do have a future interest in proof, giving Lean an edge for me. I prefer my symbolic reasoning in visual form. I anticipate a future where we draw and view AI drawings, and see any printing press derived notation as antiquated as cuneiform. The above image is a possible language for representing the first Lean proof in "The Natural Number Game". About one in ten mathematicians that I show this to can grasp it much faster than the Lean notation. The other nine imagine a visual programming language to be something like a PowerPoint slide or a children's graphics language, and don't see the point.

Reminds me of the idea of Radical Monopolies from Ivan Illich in a way. If a technology or service becomes so wide spread within society, even though many different versions of the technology or service may exist, a Radical Monopoly means that non users will suffer for their non use. Cars and non drivers in cities are the typical example. And I wonder, whether mathematicians who don't user theorem provers will soon suffer under the tyranny of the theorem provers, whether it be Lean or one of the others.

So that link(https://infosec.exchange/@0xabad1dea/117002106099986943) buried in the comments of comments sounds pretty damning.

Haven't seen much about SPARK and why3 recently, combined with frontier LLMs. It would seem easier to progressively prove properties from an actual implementation (going from absence of runtime errors to partial functional proof to full functional proof if you can beau the cost) and only focus the Lean effort on places where why3 (and its menagerie) of SMT provers give up ?

It would also seem highly agent-able since verification is very modular in SPARK.

I had not been familiar with the term "Dumey microsecond".

For those who found it interesting, perhaps you will also find this term enjoyable https://en.wikipedia.org/wiki/Kairos for its similarity.

Recent posts on formal proofs usually talk about Lean, Rocq, Isabelle and (due to this post) Metamath.

What do people think of F* [1]? At least, for non-mathematics projects, doesn't it seem to be a more appropriate option [2]? It seems even the CS community is gravitating towards Lean.

[1] https://fstar-lang.org/

[2] https://fstarlang.github.io/lowstar/html/Introduction.html

Was genuinely expecting an article about manufacturing methodologies! Very interesting teachable moment for me, I've always wanted to learn more about Set Theory.

Recently I was playing around in this space and came across Dafny, rather I should confess that Claude code pointed be to it.

For software projects it seemed very approachable, even for a complete newbie like me. Probably not for Math though.

Isn't it today/wouldn't it be in the close future relatively trivial to port most of the already formalized results between languages with help of LLMs?

> Metamath is based on set theory, and would therefore address some concerns one might have with the propositions-as-types philosophy used by Lean

Isn't the entire point mathematicians adopted Lean where they spurned Haskell is because of the batteries-included ZFC object language in the former? Metamath implements a set theory object language just the same, it's not based on it at all in this sense. You just changed one metalanguage for another.