Big Math and the one-brain barrier: the tetrapod model of mathematical knowledge

DOI10.1007/s00283-020-10006-0zbMath1493.68391OpenAlexW3097104763MaRDI QIDQ2663667

William M. Farmer, Jacques Carette, Michael Kohlhase, Florian Rabe

Publication date: 19 April 2021

Published in: The Mathematical Intelligencer (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/s00283-020-10006-0

zbMATH Keywords

Big Math

Mathematics Subject Classification ID

Philosophy of mathematics (00A30) Development of contemporary mathematics (01A65) Methodology of mathematics (00A35) Future perspectives in mathematics (01A67) Computer science support for mathematical research and practice (68Vxx)

Related Items (1)

\(\text{OntoMath}^{\text{PRO}}\) 2.0 ontology: updates of formal model

Uses Software

• Coq
• GAP
• Isabelle
• Mathematica
• SageMath
• Isabelle/jEdit
• HOL Light
• Automath
• MMT
• OEIS
• IMPS
• Flyspeck
• dedukti
• Lean
• GitHub
• kepler98
• MathOverflow
• PlanetMath
• MathML

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• A scalable module system
• The \(L\)-functions and Modular Forms Database project
• Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
• IMPS: An interactive mathematical proof system
• A proof of the Kepler conjecture
• The Lean Theorem Prover (System Description)
• The Isabelle Framework
• Every Planar Map is Four Colorable
• Virtual Theories – A Uniform Interface to Mathematical Knowledge Bases
• QED Reloaded: Towards a Pluralistic Formal Library of Mathematical Knowledge
• A FORMAL PROOF OF THE KEPLER CONJECTURE
• A Machine-Checked Proof of the Odd Order Theorem
• MKM
• Computational logic and the social

This page was built for publication: Big Math and the one-brain barrier: the tetrapod model of mathematical knowledge