ES version is available. Content is displayed in original English for accuracy.
Advertisement
Advertisement
⚡ Community Insights
Discussion Sentiment
75% Positive
Analyzed from 948 words in the discussion.
Trending Topics
#metamath#https#lean#language#zfc#github#html#proof#different#non
Discussion (14 Comments)Read Original on HackerNews
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
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
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
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.
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.
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.
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 isomorphic foundation, so long as you have an implementation.
Have a look at Dutch cities for how to avoid this.
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.