4 ms·

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 la

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 8y ago
Have you seen proofwiki.org?
BucketSort 8y 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 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://plfa.github.io/. https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspondence https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspon... being one of the profound ideas here.
dane-pgp 8y ago
The "drilling down layer by layer" bit does seem quite well supported: http://us2.metamath.org:88/mpeuni/konigsberg.html 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 8y 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.

ducttapecrown 8y ago

Have you seen proofwiki.org?

BucketSort 8y 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 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://plfa.github.io/. https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspondence https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspon... being one of the profound ideas here.

dane-pgp 8y ago

The "drilling down layer by layer" bit does seem quite well supported: http://us2.metamath.org:88/mpeuni/konigsberg.html 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 8y 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.