Nice, although the derivations are a bit hard to digest for a human...
I still dream of a mathematical knowledge base in which one could drill down layer by layer until reaching basic axioms. Or let’s say you’re reading a proof and don’t understand how some step follows from the previous (happens frequently when reading papers in a foreign field). In this knowledge base you could increase the level of detail for that step to see a more detailed version of the derivation, sort of how you can zoom into Google Earth. Of course building such a web of mathematical knowledge would require an enormous amount of work, but maybe it could be crowdsourced like Wikipedia; e.g. someone writes a high-level proof for a theorem, and then other people could fill in the gaps in increasing levels of detail, or add references to related theorems/corollaries.
Proof assistants are like that. Check out Coq or Agda. If you aren't aware of it already, your spirit is calling for the stuff they talk about a lot in the functional programming community. See https://youtu.be/IOiZatlZtGU for example. Maybe not the best video or intro to the themes though. Wadler also just put out a book about programming language foundations in Agda - https://plfa.github.io/. https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspon... being one of the profound ideas here.
but you're right about the high-level proofs of the theorems not looking the way most people expect to see proofs.
Perhaps the way that the proofs are broken down (to be accepted by the site) makes it hard to reassemble them at a level of abstraction that is more readable.
as a non-mathematician, I would love to see mouseover hints for mathematical symbols. For example, the proof explorer has a symbol ∈ which means "is contained within". But I don't know that without consulting the "Metamath Proof Explorer Overview" page. Being able to put the definition into the proof would greatly improve accessibility to non- or novice mathematicians, IMO.
Interesting stuff, the uniformity for so many proofs is compelling.
The names/id's are pretty hard imho yet they are used everywhere, e.g "readdcli": could be about "read" or "add" at first sight. Maybe if they were a bit longer and more descriptive, less clicking on them to view what they are might be needed...
The naming system is pretty compact but also very standardized and reliable, which is important when organizing more than 10000 theorems. That one breaks down as "re + add + cl + i" for "the REals are CLosed under ADDition, Inference form". You can also mouse over the theorem name links to see a short description.
This seems very interesting and something which might catch a lot more interest than it probably will if its homepage didn't look so dated and text-heavy.
I'm very much in favor of initiatives to make math more accessible to laypeople and this is right in my ballpark, but just reading over the homepage gave me visual fatigue.
Metamath is very different from an initiative to make math more accessible. This is a specialist project to write formal/mechanical proofs of many theorems.
I would be curious to discuss how this can be useful in practice for laypeople, but I don't see any.
The way it is described (especially the emphasis on how variable substitution is used as the single primitive instead of many different techniques which can take years to learn - a phrase which is repeated many times on the website) suggests to me that accessibility to people who would not usually write proofs is a concern of the project. If it is not, the project might not be doing a good job of communicating its goals clearly.
If you ever use another proof assistant, you will find that too much documentation is much better than not enough. You can certainly skip the documentation in the main pages if you get the gist. I think Metamath is most suited for a certain kind of person, the one who asks "why" incessantly and is attracted to precision of language. The best part is that you don't need to know any mathematics at all to understand it - everything is defined in excruciating detail, so it's completely self-contained.
Too much documentation is definitely better than too little. But throwing all the documentation you have up front at a new user instead of having it tucked away where it can be easily browsed when needed can make for an intimidating first contact.
That’s incorrect. It is easy to write a program that can prove any mathematical theorem that has a finite proof. The only limitations will be speed (very, very much so) and running out of memory. The latter will always happen when the to be proven theorem is false or undecidable.
To see why that works, consider that any mathematical proof can be written in a fixed alphabet, and will be of finite length, in a proving language in which proofs can be machine-checked in finite time.
Assuming that, to prove a theorem T, loop over all strings (possible because there are countable infinite of them. An implementation will do this by increasing length of the strings), and check for each of them whether it’s a valid proof for T (an extension can check whether it’s a proof for not-T, and exit if it is)
Alternatively, to find _all_ valid theorems, loop over all strings, and check for each of them whether it’s a valid proof (that will find many, many extremely dull theorems, but assuming such theorems exist, it will find beautiful ones humans haven’t thought of, too)
I still dream of a mathematical knowledge base in which one could drill down layer by layer until reaching basic axioms. Or let’s say you’re reading a proof and don’t understand how some step follows from the previous (happens frequently when reading papers in a foreign field). In this knowledge base you could increase the level of detail for that step to see a more detailed version of the derivation, sort of how you can zoom into Google Earth. Of course building such a web of mathematical knowledge would require an enormous amount of work, but maybe it could be crowdsourced like Wikipedia; e.g. someone writes a high-level proof for a theorem, and then other people could fill in the gaps in increasing levels of detail, or add references to related theorems/corollaries.