What is the point of computers? A question for pure mathematicians

DOI10.4171/icm2022/166arXiv2112.11598OpenAlexW4389818406MaRDI QIDQ6118162

Kevin Buzzard

Publication date: 20 March 2024

Published in: International Congress of Mathematicians (Search for Journal in Brave)

Full work available at URL: https://arxiv.org/abs/2112.11598

zbMATH Keywords

proof assistanttheorem proverITP

Mathematics Subject Classification ID

Formalization of mathematics in connection with theorem provers (68V20)

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• On large subsets of \(\mathbb{F}_q^n\) with no three-term arithmetic progression
• Isabelle/HOL. A proof assistant for higher-order logic
• Distant decimals of \(\pi \): formal proofs of some algorithms computing them and guarantees of exact computation
• A verified ODE solver and the Lorenz attractor
• Inter-universal Teichmüller theory. III: Canonical splittings of the log-theta-lattice
• A corrected quantitative version of the Morse lemma
• Formalizing an analytic proof of the prime number theorem
• A Computer-Algebra-Based Formal Proof of the Irrationality of ζ(3)
• HOL Light: An Overview
• A Brief Overview of Mizar
• The Lean Theorem Prover (System Description)
• The Four Colour Theorem: Engineering of a Formal Proof
• A FORMAL PROOF OF THE KEPLER CONJECTURE
• A Machine-Checked Proof of the Odd Order Theorem
• Theorem Proving in Higher Order Logics
• Notes on elliptic curves. II.
• Nine Chapters of Analytic Number Theory in Isabelle/HOL.