What is the current state of formalized mathematics?

Russell and Whitehead famously tried to actually create and use a formal system to explicitly develop formal mathematics in their work, "Principia Mathematica."

Much more recently, with the aid of computers, there has been much work done related to the development of proof assistant software, formal verification software, and automated theorem proving software.

However, even though extensive libraries of formal proofs have been developed with all this research, I have not been able to find any attempts made to present the contents of a given library of proofs in an "updated Principia Mathematica," as a formal development of math.

Have I just not done an extensive enough literature search?

Thanks in advance!

On the one hand, there has been a lot of success recently in creating fully formalized and computer-verified proofs of nontrivial theorems, including Hales' theorem, the prime number theorem, the Jordan curve theorem, and Gödel's incompleteness theorems. The sense I get from experts in the field is that the main challenge is time, not theory. It takes a long time to formalize human-readable proofs into computer-verifiable proofs with the present systems, but there should be no theoretical obstacles to formalizing any theorem one wishes to study.

On the other hand, there are other reasons that nothing explicitly like Principia Mathematica has been developed. The first of these is that Principia is virtually unreadable. As a means of conveying mathematical information from one person to another, fully formal or even mostly formal proofs (the kind that a proof assistant can verify) are not as efficient as ordinary natural-language proofs. This means that few mathematicians have a desire to work with any "new" system of this kind. We already realize that virtually all mathematical theorems can be formalized in ZFC set theory, but instead we write proofs in a way that tries to convey the mathematical insight more than the technical details of a formal system, unless the technical details are somehow important.

There has been a lot of recent work on a different foundational system called "homotopy type theory", which could be used instead of ZFC to formalize theorems. It remains to be seen, however, whether this new system ends up being widely adopted. There other foundational systems, such as second-order arithmetic, which could also be used to fully formalize large parts of mathematics. I believe that a significant number of mathematicians don't really worry much about the foundational system they use, because the objects they deal with are sufficiently concrete that the foundations make little difference.

The other goal of Principia was to support the logicist program that all of mathematics can be reduced to logic. The idea that mathematics can be formalized and presented in full detail is no longer in question, as it might have been at the time. But the idea that the axioms of a foundational theory would all be fully logical is far from clear - in fact, it is generally considered false, because axioms such as the axiom of infinity or the axiom of replacement do not seem purely "logical" to many mathematicians.

I think that Metamath (list of mirrors) is likely the best candidate for a modern version of Principia Mathematica. The theorem list is broken up into many parts and develops:

• Propositional calculus
• ZF, ZFC, and TG (roughly the type of set theory that Mizar uses as well)
• Real and complex numbers
• Abstract algebraic structures (including category theory)
• Topology (a lot of pointset, and some basic definitions for algebraic)
• Precalculus and Calculus concepts
• and various other assorted things

Aditionally, Principia Mathematica was an inspiration for Metamath, and a major contributor made a talk on youtube a couple months after the OP's question was posted titled "Metamath Proof Explorer: A Modern Principia Mathematica".

To address @Carl Mummert's point in his answer: "Principia is virtually unreadable...few mathematicians have a desire to work with any "new" system of this kind". I agree. That said, some of those few mathematicians have been working on Metamath, regardless of how it is certainly more difficult to read in some ways than a textbook or paper.

The most promising systems as of 2019

I have talked with people in the area and gone through the description of some of the existing projects, and these seem to be the most promising projects:

• Isabelle: appears to have a very rich IDE, but the system is very complex under the hood

  A nice curated archive of Isabelle proofs can be found at: https://devel.isa-afp.org/ "Isabelle Archive of Formal Proofs".

  Isabelle source is on a self hosted Mercurial. The documentation is in PDF format. Does not have an Ubuntu package. Bad signs.

  Isabelle was notably used to prove correctness of the sel4 operating system: https://github.com/seL4/l4v

• Coq. Vs Isabelle / HOL: https://stackoverflow.com/questions/30152139/what-are-the-strengths-and-weaknesses-of-the-isabelle-proof-assistant-compared-t

  Coq source is on GitHub currently with 2k+ stars as of 2019. The documentation is in HTML format. Has an Ubuntu 19.04. package. Good signs.

  Coq was notably used in one of the Four Color Theorem proofs.

• 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

I will add more information to this list as I learn more about those systems and try them out myself.

And here are some more interesting links:

• http://www.cs.ru.nl/~freek/100/ list of how many of the "Top 100 theorems" have been proved in several formal systems
• https://github.com/awesomo4000/awesome-provable an awesome list of formal stuff

One thing which I haven't found yet, but feel is badly missing, is a package register + continuous integration website, a bit like Metamath, but that anyone can contribute to like PyPI, and which runs the proofs and shows them on the web interface. I have described this idea in a bit more detail here.