🇳🇱
Part of me wants to reconstruct all of math up to calculus from scratch and document it all and then create a knowledge map so someone can see how any advanced idea is derrived from the most elementary ideas.
Partly I want to do this for myself just because I have a hard time remembering some derrivations, particularly in calculus where you have to go back to limits to show it.
@freemo could polish http://us.metamath.org from set theory
Or there are several systems in type theory.
@jmw150 metamath is definately not just a database. It is a special language you can use to write proofs and have a system automatically verify the validity of a proof as well as render the proof as a webpage.
That ability to confirm the validity of a proof is what I usually hear people talk about when they have mentioned metamath.
@freemo it is more like a database.
Systems like Coq are more fun though I think. The standard library is proofs for a bunch of undergrad math like the dedikind cut construction of reals. Real numbers at your fingertips. 😁