...

that proves math theorems by recording every proof step as either an axiom (assumption) or previously-proved theorem. It is one of the largest databases of formalized verified mathematics even when you include math databases that do not record every proof step. These proofs are all based on a very small number of widely-accepted axioms: classical first-order logic, Zermelo-Fraenkel set theory with the axiom of choice (ZFC), and the Tarski-Grothendieck Axiom. It is rigorously computer-verified; it's been verified by five different computer-based verifiers written in five different programming languages by more than five different people. We know of no other such database that has been so thoroughly verified. This view was created by David A. Wheeler. Music is by audionautix.com - "Threshold" by Jason Shaw, CC-BY-3.0 Unported. This video (in total) is released under the Creative Commons CC-BY-3.0 Unported license. In this visualization, contributions are shown over time (the increasing date is shown at the top center). Tiny filled circles are assertions (most are proven, the near-white ones are axioms or definitions); note that there are more and more over time. The "flashes" from people to the assertions are initial contributions or modifications of some kind. The major areas (each with a different color) represent the top headings of set.mm, with branches inside the major areas representing level 2 headings. For simplicity, the section structure shown is always the structure of the 2019-10-04 version of set.mm, and assertions are shown in their respective sections in that version. The captions at the bottom-left note some significant events, such as proving a "Metamath 100" mathematical theorem (see http://us.metamath.org/mm_100.html ). The initial "big bang" effect is due in part to the 519 theorems dated 5-Aug-1993, which is when Norman Megill first added a date stamp to metamath.exe. Actually, these theorems were proved over a period of months before that date, but the version of set.mm used did not have those early dates. This view was generated using the date information in the latest version of set.mm at the time; because of this, it does not include any references to statements that were in earlier versions but later deleted. The section "CLASSICAL FIRST-ORDER LOGIC WITH EQUALITY" formally defines the logic system we use in set.mm. In particular, it defines symbols for declaring truthful statements, along with rules for deriving truthful statements from other truthful statements. But that's not enough; we need something to talk *about*. The section "ZF (ZERMELO-FRAENKEL) SET THEORY" allows us to assert properties of arbitrary mathematical objects called "sets." The section "REAL AND COMPLEX NUMBERS" derives the basics of real and complex numbers; in it we first construct real and complex numbers ("prove that numbers exist"), axiomatize them, derive their basic properties, and define important operations and subsets. Unlike the older Gource visualization through 2019-09-26, this visualization shows initial contributions AND modifications, fixes some attributions, adds captions, and has various visual improvements. While set.mm is the largest Metamath database, there are other databases such as iset.mm (which uses intuitionistic logic) not shown here. As of 2019-10-04 there have been 48 different contributors to Metamath set.mm. Those contributors were (alphabetically by full name): Alan Sare, Alexander van der Vekens, Andrew Salmon, Anthony Hart, Benoit Jubin, Brendan Leahy, Chen-Pang He, David A. Wheeler, David Abernethy, David Harvey, David Moews, Drahflow, Eric Schmidt, Fan Zheng, Filip Cernatescu, Frédéric Liné, Gérard Lang, Giovanni Mascellani, Glauco Siliprandi, Gregory Bush, Jarvin Udandy, Jason Orendorff, Jeff Hankins, Jeff Hoffman, Jeff Madsen, Jerry James, Jim Kingdon, Jon Pennant, Jonathan Ben-Naim, Jonathan Yan, Josh Purinton, Juha Arpiainen, Mario Carneiro, Mel L. O'Cat, Norman Megill, Paul Chapman, Raph Levien, Rodolfo Medina, Roy F. Longton, rpenner, Saveliy Skresanov, Scott Fenton, Stefan Allan, Stefan O'Rear, Steve Rodriguez, Szymon Jaroszewicz, Thierry Arnoux, and Wolf Lammen. You might be interested in our book, "Metamath: A Computer Language for Mathematical Proofs" by Norman Megill & David A. Wheeler, 2019, ISBN 9780359702237. http://www.lulu.com/shop/norman-megill-and-david-a-wheeler/metamath-a-computer-language-for-mathematical-proofs/hardcover/product-24129769.html A related video that introduces Metamath and set.mm is "Metamath Proof Explorer: A Modern Principia Mathematica" at https://www.youtube.com/watch?v=8WH4Rd4UKGE For more information on set.mm (Metamath Proof Explorer (MPE)), see its home page at http://us.metamath.org/mpeuni/mmset.html