Greg Egan's Diaspora has a rather good illustration of what a fully formalized mathematical system might look like. He called it the Mines[1]: a representation

Greg Egan's Diaspora has a rather good illustration of what a fully formalized mathematical system might look like. He called it the Mines[1]: a representation of the full acyclic digraph of all the theorems proved so far by a community of mathematicians. A student can examine any proposition, see if its yet been proven (and if so, how, and from what antecedents) as well as what deeper results might depend on it. Critically, a student might select a research topic simply by travelling to the ends of the Mines and start digging, or might select some not yet proven goal as an end point and start working towards it... today, each mathematician must build their own mental model of the mines by exhaustively reading all related papers - a time consuming and somewhat fallible effort. Such a comprehensive map would be one of the main benefits of formalization. The video mentioned Formal Abstracts[2], which is still getting off the ground... a similar project that has been around for a while is Metamath[3]. Metamath uses an SRS (string rewriting system[4]) to formalize much foundational mathematics. It's proof explorer is conceptually similar to Egan's Mines: a database full of theorems and connections starting from fundamental axioms and definitions. Today, Metamath only includes fairly basic results, and has not yet reached a level where it can capture the state-of-the-art in modern research mathematics the way Formal Abstracts and other systems aspire to. To be fair, no system today is really at that level yet. Coq has a good set of packages and I think is probably in the lead today. I don't know where Lean is in comparison. The aspect of formalization where it somehow lends additional credence to proofs seems less important. Famously, when Hilbert went to fully formalize Euclid's geometry, he found a missing axiom[5]. (Euclid had assumed that two circles with centers closer than their radii would intersect at somewhere... which is not true over the field of rational numbers! Therefore this requires an explicit axiom, which had been overlooked for 2,000 years!) This seems to be the exception rather than the rule... as far as I know, no important theorem has been "overturned" as a result of formalization efforts. [1]: http://kasmana.people.cofc.edu/MATHFICT/mfview.php?callnumber=mf16 http://kasmana.people.cofc.edu/MATHFICT/mfview.php?callnumbe... [2]: https://formalabstracts.github.io/ https://formalabstracts.github.io/ [3]: http://us.metamath.org/mpeuni/mmset.html http://us.metamath.org/mpeuni/mmset.html [4]: https://en.wikipedia.org/wiki/Rewriting#String_rewriting_systems https://en.wikipedia.org/wiki/Rewriting#String_rewriting_sys... [5]: https://math.stackexchange.com/questions/2074781/can-we-really-intersect-circles/2076491 https://math.stackexchange.com/questions/2074781/can-we-real...