Mathematics and the formal turn

DOI10.1090/bull/1832arXiv2311.00007OpenAlexW4391839106MaRDI QIDQ6130523

Jeremy Avigad

Publication date: 3 April 2024

Published in: Bulletin of the American Mathematical Society (Search for Journal in Brave)

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

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Mechanization of proofs and logical operations (03B35) General topics in artificial intelligence (68T01) Formalization of mathematics in connection with theorem provers (68V20) Computer-assisted instruction, e-learning (aspects of mathematics education) (97U50) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15) Digital mathematics libraries and repositories (68V35) Presentation and content markup for mathematics (68V25)

Cites Work

• A revision of the proof of the Kepler conjecture
• A verified ODE solver and the Lorenz attractor
• Formally verified approximations of definite integrals
• A formalization of Dedekind domains and class groups of global fields
• The sphere packing problem in dimension \(24\)
• A corrected quantitative version of the Morse lemma
• A proof of the Kepler conjecture
• Turing's Legacy
• Developments in Formal Proofs
• Verifying Nonlinear Real Formulas Via Sums of Squares
• Opinion: The Mechanization of Mathematics
• Advancing mathematics by guiding human intuition with AI
• Notices of the American Mathematical Society
• MODULARITY IN MATHEMATICS
• A FORMAL PROOF OF THE KEPLER CONJECTURE
• Type Classes and Filters for Mathematical Analysis in Isabelle/HOL
• The resolution of Keller's conjecture
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: Mathematics and the formal turn