Metamath

http://us.metamath.org/

by lainon • 7 years ago

167 19 7 years ago

us.metamath.org

pcstl4• 7 years ago

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.

erwan577• 7 years ago

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.

pcstl4• 7 years ago

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.

digama03• 7 years ago

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.

pcstl4• 7 years ago

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.

rambojazz• 7 years ago

I'll take text-heavy over javascript-heavy any day.

pcstl4• 7 years ago

Sure, same here. However, I’m not talking about that tradeoff. I’m talking about organizing all the text a little better.

aaaaaaaaaaab• 7 years ago

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.

ducttapecrown• 7 years ago

Have you seen proofwiki.org?

BucketSort• 7 years ago

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.

dane-pgp• 7 years ago

The "drilling down layer by layer" bit does seem quite well supported:

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.

appleflaxen• 7 years ago

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.

Aardwolf• 7 years ago

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...

digama03• 7 years ago

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.

jewelry• 7 years ago

I thought everyone knows that Hilbert proved that it's impossible for machine to prove any theorem that human don't already know...

digama03• 7 years ago

Only if you're an ideal rational agent. Maths is hard.

smadge• 7 years ago

The proofs in Metamath are not produced by machines. Humans write them, but machines validate them.

Someone• 7 years ago

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)

DoctorOetker• 7 years ago

thats just utter nonsense. furthermore what would have been this magic time of "already" ? that alone should have triggered your own bs alert...

Metamath

Related Stories