When Ciro Santilli first learnt the old Zermelo-Fraenkel set theory and the idea of formal proofs, his teenager mind was completely blown.

Finally, there it was: a proper and precise definition of mathematics, including a definition of integers, reals and limits!

Theorems are strings, proofs are string manipulations, and axioms are the initial strings that you can use.

Once proved, press a button on your computer, and the proof is automatically verified. No messy complicated "group of savants" reading it for 4 years and looking for flaws!

There are a few formal proof systems with several theorems in their Git tracked standard library. The hottest ones are:

- https://github.com/HOL-Theorem-Prover/HOL
- https://github.com/seL4/isabelle. Rumours have it that this is "uncompilable" from source without blobs. It does however offer a very rich IDE.
- https://github.com/coq/coq
- Metamath this one is likely an older and less powerful system, but the web presentation and tutorial are very good! Source: https://github.com/metamath/metamath-exe Here is a proof that 2 + 2 equals 4: http://us.metamath.org/mpeuni/2p2e4.html
- https://en.wikipedia.org/wiki/Lean_(proof_assistant) | https://github.com/leanprover/lean | https://github.com/leanprover/lean4

And here are some more interesting links:

- https://github.com/awesomo4000/awesome-provable an awesome list of formal stuff
- https://devel.isa-afp.org/ Isabelle Archive of Formal Proofs. A curated list of Isabelle proofs, with minimal web UI. This is almost what we need, but without the manual curation, and with a better web UI.
- http://www.cs.ru.nl/~freek/100/ list of how many of the "Top 100 theorems" had been proved in several formal systems.

However, as expressed by the QED manifesto, is unbelievable that there isn't one awesome and dominating website, that hosts all those proofs, possibly an on the browser editor, and which all mathematicians in the world use as the one golden reference of mathematics to rule them all!

Just imagine the impact.

Standard library maintainers don't have to deal with the impossible question of what is "beautiful" or "useful" enough mathematics to deserve merged: users just push content to the online database, and star what they like!

Interested in a conjecture? No problem: just subscribe to its formal statement + all known equivalents, and get an email on your inbox when it gets proved!

Are you a garage mathematician and have managed to prove a hard theorem, but no will will read your proof? Fuck that, just publish it on the system and let it get auto verified. Overnight fame awaits.

Notation incompatibility hell? A thing of the past, just automatically convert to your preferred representation.

Such a system would be the perfect companion to Write free books to get famous website. Just like computer code offers the backbone of Linux Kernel Module Cheat Linux kernel tutorials, a formal proof system website would be the backbone of mathematics tutorials! You know what, if Write free books to get famous website becomes insanely sucessful, Ciro is going to add this to it later on.

Furthermore, it would not be too hard to achieve this system!

All we would need would be something analogous to a package registry like PyPI or NodeJS' registry.

Then, each person can publish packages containing proofs.

Packages can rely on other packages that contain pre-requisites definition or theorem.

Packages are just regular git repos, with some metadata. One notable metadata would be a human readable description of the theorems the package provides.

The package registry would then in addition to most package registries have a CI server in it, that checks the correctness of all proofs, generates a web-page showing each theorem.

All proofs can be conditional: the package registry simply shows clearly what axiom set a theorem is based on.

This is a close as we can get to ErdΕs' book.

Maybe Ciro will just stuff this into Write free books to get famous website once that takes over the world.

Bibliography:

- https://math.stackexchange.com/questions/1767070/what-is-the-current-state-of-formalized-mathematics/3297536#3297536
- https://stackoverflow.com/questions/19421234/how-do-i-generate-latex-from-isabelle-hol
- https://stackoverflow.com/questions/30152139/what-are-the-strengths-and-weaknesses-of-the-isabelle-proof-assistant-compared-t

- The most important projects Ciro Santilli wants to do | 46, 2k, 4
- Ciro Santilli | 514, 53k, 177
- Ciro Santilli's Homepage | 238, 154k, 2k

- Formalization of Mathematics | 439, 818, 20
- QED manifesto | 25