The text above includes direct links to specific documents and references. Here we’ll give a slightly more general bibliography, though most of it should be considered background, since the approach taken here represents a significant departure from traditional directions, and builds more or less directly on extremely low-level concepts.

The earliest known large-scale axiomatic presentation of mathematics was:

Euclid (300 BC), Στοιχεῖα (in Ancient Greek) [

*Elements*].Empirical metamathematics from this was given in:

The concept that there is underlying reality in mathematics was discussed in:

Plato (375 BC),

*πολιτεία (in Ancient Greek) [**The Republic*].Plato (360 BC),

*Τίμαιος (in Ancient Greek) [**Timaeus*].Modern explorations of these ideas include:

M. Balaguer (1998),

*Platonism and Anti-Platonism in Mathematics*, Oxford University Press.J. Gray (2008),

*Plato’s Ghost: The Modernist Transformation of Mathematics,*Princeton University Press.R. Tieszen (2011),

*After Gödel: Platonism and Rationalism in Mathematics and Logic*, Oxford University Press.The contemporary axiomatic formulation of mathematics was developed in:

F. L. G. Frege (1879),

*Begriffsschrift: eine der arithmetischen nachgebildete Formelsprache des reinen Denkens*(in German), Verlag von Louis Neber. (Translated in J. v. Heijenoort (1967), as “Begriffsschrift: A Formal Language, Modeled upon That of Arithmetic, for Pure Thought” in*From Frege to Gödel: A Source Book in Mathematical Logic, 1879–1931*,*Harvard University Press, 1–82.)*R. Dedekind (1888),

*Was sind und was sollen die Zahlen?*(in German), F. Vieweg und Sohn. (Translated in H. Pogorzelski, et al. (1995), as*What Are Numbers and What Should They Be?*,*Research Institute for Mathematics.)*G. Peano (1889),

*Arithmetices principia, nova methodo exposita*(in Italian), Fratres Bocca. (Translated by H. C. Kennedy (1973), as “The Principles of Arithmetic, Presented by a New Method”, in*Selected Works of Giuseppe Peano*,*University of Toronto Press, 101–134.)*D. Hilbert (1903),

*Grundlagen der geometrie*(in German), B. G. Teubner. (Translated by E. G. Townsend (1902), as*The Foundations of Geometry*, Open Court.)E. Zermelo (1908), “Untersuchungen über die Grundlagen der Mengenlehre I” (in German),

*Mathematische Annalen*65: 261–281. doi:10.1007/BF01449999. (Translated by J. v. Heijenoort (1967), as “Investigations in the Foundations of Set Theory” in*From Frege to Gödel: A Source Book in Mathematical Logic, 1879–1931*, Harvard University Press, 199–215.)A. N. Whitehead and B. A. W. Russell (1910–1913),

*Principia Mathematica, Volumes I–III*, Cambridge University Press.A standard collection of source documents is:

J. v. Heijenoort (1967),

*From Frege to Gödel: A Source Book in Mathematical Logic, 1879–1931,*Harvard University Press.Among general commentaries on axiomatic formalism are:

N. Bourbaki (1950), “The Architecture of Mathematics”,

*The American Mathematical Monthly*57: 221–232. doi: 10.2307/2305937.S. Feferman, et al. (2000), “Does Mathematics Need New Axioms?”,

*The**Bulletin of Symbolic Logic 6*, 401-446. doi: 10.2307/420965.W. Sieg (2013),

*Hilbert’s Programs and Beyond*, Oxford University Press.A. Weir (2019), “Formalism in the Philosophy of Mathematics”,

*The Stanford Encyclopedia of Philosophy*, plato.stanford.edu/archives/spr2022/entries/formalism-mathematics.Expositions of metamathematics and mathematical logic ideas appear for example in:

D. Hilbert and W. Ackermann (1928),

*Grundzüge der theoretischen Logik*(in German)*,*Springer. (Translated by L. M. Hammond, et al. (2000), as*Principles of Mathematical Logic*, AMS Chelsea.)W. V. O. Quine (1940),

*Mathematical Logic*, W. W. Norton & Company.A. Church (1956),

*Introduction to Mathematical Logic,*Princeton University Press.H. Wang (1962),

*A Survey of Mathematical Logic*, Science Press North-Holland.H. B. Curry (1963),

*Foundations of Mathematical Logic*, Dover.H. Rasiowa (1963),

*The Mathematics of Metamathematics*, Panstwowe Wydawnictwo Naukowe.E . Mendelson (1964),

*Intro to Mathematical Logic*, Van Nostrand Reinhold.G. Kreisel and J. L. Krivine (1967),

North-Holland.

*Elements of Mathematical Logic: Model Theory,*North-Holland.

S. C. Kleene (1971),

*Introduction to Metamathematics*, Wolters-Noordhoff.H. B. Enderton (1972),

*A Mathematical Introduction to Logic*, Harcourt/Academic Press.A. Yasuhara (1975), “Recursive Function Theory and Logic”,

*Journal of Symbolic Logic*40: 619–620. doi: 10.2307/2271829.J. Barwise (1982),

*Handbook of Mathematical Logic*, Elsevier.G. E. Sacks (2003),

*Mathematical Logic in the 20th Century*, World Scientific.Works on the metamodeling of mathematics and on universal algebra include:

A. N. Whitehead (1898),

*A Treatise on Universal Algebra with Applications*, Cambridge University Press.A. Robinson (1963),

*Introduction to Model Theory and to the Metamathematics of Algebra*, North-Holland.N. G. de Bruijn (1970), “The Mathematical Language AUTOMATH, Its Usage, and Some of Its Extensions”, in

*Symposium on Automatic Demonstration*, M. Laudet, et al. (eds.), Springer.A. I. Mal’Cev (1971),

*The Metamathematics of Algebraic Systems, Collected Papers: 1936–1967*, North-Holland.A. S. Toelstra (1973),

*Metamathematical Investigation of Intuitionistic Arithmetic and Analysis*, Springer.S. Burris and H. P. Sankappanavar (1981),

*A Course in Universal Algebra*, Springer.Low-level symbolic representations of mathematics were developed in:

M. Schönfinkel (1924), “Über die Bausteine der mathematischen Logik” (in German),

*Mathematische Annalen*92, 305–316. doi: 10.1007/BF01448013. (Translated by S. Bauer-Mengelberg (1967), as “On the Building Blocks of Mathematical Logic”, in*From Frege to Gödel: A Source Book in Mathematical Logic, 1879–1931*, J. v. Heijenoort, Harvard University Press, 357–366.)E. Post (1936), “Finite Combinatory Processes—Formulation 1”,

*The Journal of Symbolic Logic*1, 103–105. doi: 10.2307/2269031.See also these commentaries:

S. Wolfram (2020), “Combinators and the Story of Computation”. arXiv: 2102.09658.

S. Wolfram (2021),

*Combinators: A Centennial View,*Wolfram Media*.*S. Wolfram (2021), “After 100 Years, Can We Finally Crack Post's Problem of Tag? A Story of Computational Irreducibility, and More”. arXiv: 2103.06931.

Practical representation of mathematics using symbolic transformations was developed in:

S. Wolfram, et al. (1981),

*SMP: A Symbolic Manipulation Program*. stephenwolfram.com/publications/smp-symbolic-manipulation-program.S. Wolfram (1988),

*Mathematica: A System for Doing Mathematics by Computer*, Addison-Wesley.Wolfram Research (1988), Mathematica [Software system]. wolfram.com/mathematica.

Wolfram Research (2013), Wolfram Language [Computational language].

wolfram.com/language.

wolfram.com/language.

A proof of the “arithmeticization of metamathematics” was given in:

K. Gödel (1931), “Über formal unentscheidbare Sätze der

*Principia Mathematica*und verwandter Systeme, I” (in German),*Monatshefte für Mathematik und Physik*38: 173–198. doi: 10.1007/BF01700692. (Translated by B. Meltzer (1992), as*On Formally Undecidable Propositions of Principia Mathematica and Related Systems*, Dover.)A major precursor to this work is:

S. Wolfram (2002), “Implications for Mathematics and Its Foundations”, in

*A New Kind of Science*, Wolfram Media, 772–821. wolframscience.com/nks/p772--implications-for-mathematics-and-its-foundations.Our Physics Project is described in:

S. Wolfram (2020),

*A Project to Find the Fundamental Theory of Physics*, Wolfram Media.S. Wolfram (2020), “A Class of Models with the Potential to Represent Fundamental Physics”,

*Complex Systems*29: 107–536. doi: 10.25088/ComplexSystems.29.2.107 and arXiv:2004.08210.The Wolfram Physics Project [Website] wolframphysics.org.

The concept of the ruliad was introduced in:

S. Wolfram (2021), “The Concept of the Ruliad”. writings.stephenwolfram.com/2021/11/the-concept-of-the-ruliad.

The concept of the mathematical observer was introduced in:

S. Wolfram (2021), “What Is Consciousness? Some New Perspectives from Our Physics Project”. writings.stephenwolfram.com/2021/03/what-is-consciousness-some-new-perspectives-from-our-physics-project.

S. Wolfram (2021), “Why Does the Universe Exist? Some Perspectives from Our Physics Project”. writings.stephenwolfram.com/2021/04/why-does-the-universe-exist-some-perspectives-from-our-physics-project.

Automated theorem proving is discussed for example in:

A. Robinson and A. Voronkov (2001),

*Handbook of Automated Reasoning: Volume I,*Elsevier.Relevant Wolfram Language functions include:

Wolfram Research (2018), FindEquationalProof, Wolfram Language function,

reference.wolfram.com/language/ref/FindEquationalProof.html (updated 2020).

reference.wolfram.com/language/ref/FindEquationalProof.html (updated 2020).

Wolfram Research (2019), AxiomaticTheory, Wolfram Language function,

reference.wolfram.com/language/ref/AxiomaticTheory.html (updated 2021).

reference.wolfram.com/language/ref/AxiomaticTheory.html (updated 2021).

A system for low-level proof-oriented formalized mathematics (used here for empirical

metamathematics) is:

metamathematics) is:

N. Megill (1993), Metamath [Software system]. us.metamath.org/index.html.

N. Megill and D. A. Wheeler (2019),

*Metamath: A Computer Language for Mathematical Proofs,*Lulu.Other systems for proof-oriented formalized mathematics include:

N. G. de Brujin (1967), Automath [Software system]. win.tue.nl/automath.

A. Trybulec (1973), Mizar [Software system]. mizar.uwb.edu.pl.

University of Cambridge and Technical University of Munich (1986), Isabelle [Software system]. isabelle.in.tum.de.

T. Coquand and G. Huet (1989), Coq [Software system]. coq.inria.fr.

U. Norell and C. Coquand (2007), Agda [Software system]. wiki.portal.chalmers.se/agda/pmwiki.php.

Microsoft Research (2013), Lean [Software system]. leanprover.github.io.

Discussions of formalized mathematics include:

H. Wang (1960), “Toward Mechanical Mathematics”,

*IBM Journal of Research and Development*4: 2–22. doi: 10.1147/rd.41.0002.H. Friedman (1997), “The Formalization of Mathematics.” cpb-us-w2.wpmucdn.com/u.osu.edu/dist/1/1952/files/2014/01/TalkFormMath12pt1.2.97-2jlte5o.pdf.

T. C. Hales (2008), “Formal Proof”,

*Notices of the AMS*55: 1370–1380. ams.org/notices/200811/tx081101370p.pdf.J. Avigad and J. Harrison (2014), “Formally Verified Mathematics”,

*Communications of the ACM*57: 66–75. doi: 10.1145/2591012.M. Ganesalingam and W. T. Gowers (2017), “A Fully Automatic Theorem Prover with Human-Style Output”,

doi: 10.1007/s10817-016-9377-1.

*Journal of Automated Reasoning*58: 253–291.doi: 10.1007/s10817-016-9377-1.

S. Wolfram (2018), “Logic, Explainability and the Future of Understanding”.

writings.stephenwolfram.com/2018/11/logic-explainability-and-the-future-of-understanding.

writings.stephenwolfram.com/2018/11/logic-explainability-and-the-future-of-understanding.

K. Buzzard (2021), “What Is the Point of Computers? A Question for Pure Mathematicians”. arXiv: 2112.11598.

Books on the philosophy of mathematics and its foundations include:

P. Benacerraf and H. Putnam (eds.) (1964),

*Philosophy of Mathematics: Selected Readings,*Prentice-Hall.I. Lakatos (1976),

*Proofs and Refutations: The Logic of Mathematical Discovery*, Cambridge University Press.T. Tymoczko (1986),

*New Directions in the Philosophy of Mathematics*, Birkhäuser.S. Shapiro (2000),

*Thinking about Mathematics: The Philosophy of Mathematics*, Oxford University Press.R. Krömer (2007),

*Tool and Object: A History and Philosophy of Category Theory*, Springer.E. Grosholz and H. Breger (2013),

*The Growth of Mathematical Knowledge*, Springer.The philosophical study of mathematics in terms of interrelated structure is summarized in:

E. Reck and G. Schiemer (2019), “Structuralism in the Philosophy of Mathematics”,

*The Stanford Encyclopedia of Philosophy.*plato.stanford.edu/archives/spr2020/entries/structuralism-mathematics.The structure of proof space is discussed in univalent foundations and homotopy

type theory:

type theory:

The Univalent Foundations Program (2013),

Advanced Study.

*Homotopy Type Theory*, Institute forAdvanced Study.

S. Awodey, et al.

*(2013), “Voevodsky’s Univalence Axiom in Homotopy Type Theory”,**Notices of the AMS*60: 1164–1167. doi: 10.48550/arxiv.1302.4731.S. Awodey (2014), “Structuralism, Invariance, and Univalence”,

*Philosophia Mathematica*22: 1–11. doi: 10.1093/philmat/nkt030.M. Shulman (2021), “Homotopy Type Theory: The Logic of Space” in

*New Spaces in Mathematics: Volume 1 Formal and Conceptual Reflections*, M. Anel and G. Catren (eds.), Cambridge University Press.Relations between category theory, mathematics and our Physics Project were explored in:

X. D. Arsiwalla, J. Gorard, and H. Elshatlawy (2021), “Homotopies in Multiway (Non-deterministic) Rewriting Systems as

*n*-Fold Categories”. arXiv:2105.10822.X. D. Arsiwalla and J. Gorard (2021), “Pregeometric Spaces from Wolfram Model Rewriting Systems as Homotopy Types”. arXiv:2111.03460.