Are We Stuck with Lean?
mathoverflow.net
Are We Stuck with Lean?
1–10 of 73 posts
Re: Are We Stuck with Lean?
#2Metamath'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
Re: Are We Stuck with Lean?
#3> 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.
Re: Are We Stuck with Lean?
#4Metamath 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
Re: Are We Stuck with Lean?
#5So that link(https://infosec.exchange/@0xabad1dea/117002106099986943) buried in the comments of comments sounds pretty damning.
Re: Are We Stuck with Lean?
#6Metamath 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: htt…
What semantics do you use for your HOL library? I scanned around but documentation on that page is a bit sparse. The github repo goes to a random user's page, and all I could find there was this unrelated repo: https://github.com/digama0/HOL
Re: Are We Stuck with Lean?
#7I 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.
Re: Are We Stuck with Lean?
#8Reminds 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.
Re: Are We Stuck with Lean?
#9Metamath 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: htt…
What semantics do you use for your HOL library? I scanned around but documentation on that page is a bit sparse. The github repo goes to a random user's page, and all I could find there was this unrelated repo: https://github.com/digama0/HOL
Yeah, that github URL should be fixed. The HOL database is here https://github.com/metamath/set.mm/blob/develop/hol.mm
Re: Are We Stuck with Lean?
#10I 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…
> lean4 doesn't let them formalize results outside of zfc.
A small correction: Lean 4's native semantics are DTT, not ZFC. Formalizing results for TT is arguably easier, it's the default. But you can use it for any foundation, so long as you have an implementation.