For anyone interested in formal verification, there's this super slick project Metamath Zero [0] by Mario Carneiro that is working to implement a verifier that

For anyone interested in formal verification, there's this super slick project Metamath Zero [0] by Mario Carneiro that is working to implement a verifier that can verify itself, compiled binary and all. As discussed on the project page, Lean is aimed at being ergonomic but at the price of a large (and somewhat buggy) codebase. On the opposite end of the spectrum is Metamath [1] which aims at being the minimum needed for formal verification, but at the cost of extremely pedantic (albeit interesting!) proofs. Metamath Zero, attempts to find a happier balance by designing a language which is both ergonomic for the proof-writer as well as minimal enough to allow self-verification. At the moment, the project is still pretty alpha but Mario is both extremely talented and actively developing. That said, if you are someone like me and just want to dive into the math, definitely check out Metamath [1]. It's library of proofs for standard ZFC foundations, set.mm [2], is seriously impressive. I mean, you can find a proof of the fundamental theorem of calculus and trace it all the way back to axioms if you so please (see theorems ftc1 [3] and ftc2 [4])! For someone with a background in math, the set.mm [2] database is an absolute blast to rogue around in. It takes some getting used to, but I am starting to prefer set.mm over Wikipedia when applicable. Anyway, I love this stuff! [0]:https://3g2upl4pq6kufc4m.onion/html?q=metamath%20zero https://3g2upl4pq6kufc4m.onion/html?q=metamath%20zero [1]:http://us.metamath.org/mm.html http://us.metamath.org/mm.html [2]:https://github.com/metamath/set.mm https://github.com/metamath/set.mm [3]:http://us.metamath.org/mpeuni/ftc1.html http://us.metamath.org/mpeuni/ftc1.html [4]:http://us.metamath.org/mpeuni/ftc2.html http://us.metamath.org/mpeuni/ftc2.html