Metamath
us.metamath.org
us.metamath.org
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.
http://us2.metamath.org:88/mpeuni/konigsberg.html
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.
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...
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.
I would be curious to discuss how this can be useful in practice for laypeople, but I don't see any.
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)