Join the discussion
Write your take first — we'll ask for email only when you're ready to publish.
- Hacker News
- > 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.
by ux266478 - I don't think Haskell would have been useful anyway? You'd want a dependently typed language for this, not Haskell. Haskell's types can't really express anything non-trivial.by eru
- 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.
by touisteur - Was genuinely expecting an article about manufacturing methodologies! Very interesting teachable moment for me, I've always wanted to learn more about Set Theory.by dieselgate
- 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?by or_am_i
- 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.
[2] https://fstarlang.github.io/lowstar/html/Introduction.html
by ducktective - So that link(https://infosec.exchange/@0xabad1dea/117002106099986943) buried in the comments of comments sounds pretty damning.by IsTom
- https://lipn.info/@mevenlennonbertrand/116997927457012577 , you and they might be jumping to conclusionsby HappyPanacea
- 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.by knuckleheads
- > Cars and non drivers in cities are the typical example.
Have a look at Dutch cities for how to avoid this.
by eru - 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.
by Syzygies - 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
by 7373737373 - My favorite minimalistic example of the Metamath base language (which higher level languages can compile down to), which, saved as, say, prop.mm can be verified with the verifier:
$c wff $. $( we use this $constant as a type of formula (well formed formula) $) $c ( ) ! -> $. $( brackets, negation, implication $) $v A B C $. $( $variables to be used in formulas $) wa $f wff A $. $( $floating hypothesis "wa" which says, that A is a well-formed formula $) wb $f wff B $. wc $f wff C $. $( The following assertions define the rules to create formulas $) $( In Metamath (unlike Metamath Zero), definitions also use the $axiom statement type $) wng $a wff ! A $. $( "not A is a well-formed-formula" - mandatory hypotheses are (wa) $) wim $a wff ( A -> B ) $. $( "A implies B is a well-formed-formula" - mandatory hypotheses are (wa, wb) $) $c |- $. $( this $constant will be used as a type of provable formula $) $( Schemes of $axioms of propositional logic $) a1 $a |- ( A -> ( B -> A ) ) $. a2 $a |- ( ( A -> ( B -> C ) ) -> ( ( A -> B ) -> ( A -> C ) ) ) $. a3 $a |- ( ( ! A -> ! B ) -> ( B -> A ) ) $. $( Definition of the Modus Ponens rule of inference in new scope; otherwise $essential hypotheses (inputs) mp1, mp2 will become mandatory for all upcoming assertions $) ${ mp1 $e |- A $. mp2 $e |- ( A -> B ) $. mp $a |- B $. $( mandatory hypotheses of "mp" are (wa, wb, mp1, mp2) $) $} $( A $proof states the string of symbols to be proven, followed by a list of labels used by the stack machine $) $( $floating and $essential hypotheses are pushed onto the top of the stack, $axioms and $proofs transform it by using the top of the stack as inputs $) $( When the stack is empty at the end, the proof is successful, and the proved statement can be reused in further proofs using its label $) $( " A implies ( B implies C) is a well-formed-formula" $) formula1 $p wff ( A -> ( B -> C ) ) $= wa wb wc wim wim $. $( "( A -> A ) -> ( A -> A ) is true (follows from the axioms)" $) formula2 $p |- ( ( A -> A ) -> ( A -> A ) ) $= wa wa wa wim wim wa wa wim wa wa wim wim wa wa a1 wa wa wa a2 mp $.by 7373737373 - According to [0], "Rocq’s kernel spans approximately 41K lines of OCaml code, while Lean’s kernel consists of approximately 8K lines of C++ code."by wk_end
- 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.
by seanhunter - Presumably because of potential network effects that would result from everyone being able to work in a single system. I don't think it's strange or implausible for people to want that.by andrewflnr
- > 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.
by ux266478 - I think it’s a lot like R vs SAS or Python and not any departure from the norm.
Mathematicians are not highly technical users that generally like programming. If you give them a path of importing someone else’s work they’ll do that instead of redoing it in their theorem prover of choice.
See the old mathematician joke:
A mathematician is asked to make tea. They take the kettle from the shelf, fill it with water, put it on the stove, turn on the heat and boil the water, then pour it into a cup.
The next day someone asks the mathematician to make tea again. The kettle is still on the stove from yesterday and there’s some leftover water in it, enough for tea.
The mathematician dumps the kettle out and puts the it away on the shelf. The mathematician says the system is in a known previously solved state and therefore trivially solved.
Now substitute 1500 lines of coq or lean for the kettle. As far as I know the outputs aren’t interchangeable like a vim or eMacs text file.
by data-ottawa - Agreed. In addition I think a big reason why we are discussing formalization so much at the moment is that it has only recently become viable to do large scale formalization of mainstream mathematics, using LLMs. These same LLMs will make it much easier to translate from one language to another and port even larger codebases over.
My prediction would therefore be that the LLMs will let us work more-or-less using standard mathematical prose that then gets to codified to some machine-readable and checkable language, but what the language used by the proof checker actually is will be more of a technical detail. In particular, I suspect people will not care too much about the language used for proofs themselves, which means that we might allow for more boilerplate if it is faster to elaborate/compile, unlike current interactive theorem provers which are meant to ease the work of humans. How the language looks like for the statements of the theorems and definitions is probably more important however, since humans will want still to be able to check that what is being formalized corresponds to what they had in mind.
by quasisphere - I have zero experience with formal verification, just speculating here - but could it be because of the network effects?
More users on your preferred tool means a more comprehensive database of existing proofs, and that makes writing new proofs easier, right?
by pverheggen - > It feels exactly like if all the emacs users in the world tried to force all vim users to use emacs.
That's why emacs has a vim mode[1].
by Balooga - > It feels exactly like if all the emacs users in the world tried to force all vim users to use emacs.
I don't know about forcing, but there's certainly a long history of emacs users trying to convince vim users that they're wrong. Without loss of generality - the same is true in the other direction of course.
Software devs are more than used to having a multitude of tools at our disposal (text editors, programming languages, Linux distros...), having strong preferences, and engaging in the delicate balancing act of advocating for our favourites while living-and-letting-live as the cosmic ballet goes on. It's part of our culture; I don't think that culture necessarily exists outside. For instance, a common layman question to ask is, "Why are there so many programming languages? Why doesn't everyone just use the same one?" And I don't think mathematicians are immune to this blind spot.
The nearest equivalent to "tooling" in math, traditionally, would be notation I suppose, and mathematicians are accustomed to eventually coalescing around a single standard notation.
by wk_end - 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
by dwheeler - There are other forms of logic? is intuitionistic logic as rigorous? fascinating
edit: the link says it is a weakening. if it is weakened, how can you prove the same stuff? i am a bit confused but i can see how it is useful for smarter people than me!
by SpaceManNabs - 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/HOLby ux266478
- Metamath is interesting for education in the principles of formal proofs, because:
1. The Metamath Book is self-contained well written, simple introduction.
2. Everything is explicit, nothing is hidden.
3. Because of extremely simple syntax and semantics it's easy write own proof verifier.
The drawbacks are:
1. Non-standard approach to free and bound variables.
2. Very weak logic in comparison to Lean. The logical syntax rules and logical semantics rules used for proving mathematical statements in Metamath, have to be explicitly specified in the Metamath database. In Lean they are part of the Lean kernel. An bug in this Metamath specification is equivalent to a bug in Lean kernel.
3. Almost no proof automation. No tactics. Long, hard to read proofs.
I would characterize Metamath as the assembly language of proof assistants, very low level and detailed way to write proofs.
by leonidasrup