Algorithm and abstraction in formal mathematics

DOI10.1007/978-3-031-64529-7_2MaRDI QIDQ6637783zbMATH OpenFDO

Authors Heather Macbeth

Publication date 13 November 2024

Full work available at URL https://doi.org/10.1007/978-3-031-64529-7_2

Mathematics Subject Classification ID

Computer science support for mathematical research and practice (68Vxx)

Cites work

• A Down-to-Earth View of Mathematics
• A formal proof of the Kepler conjecture
• A formalization of the change of variables formula for integrals in mathlib
• A machine-checked proof of the odd order theorem
• A mathematician's apology.
• A verified ODE solver and the Lorenz attractor
• Abstraction boundaries and spec driven development in pure mathematics
• Are these the most beautiful?
• Automating Elementary Number-Theoretic Proofs Using Gröbner Bases
• Beauty is not simplicity: an analysis of mathematicians' proof appraisals
• Competing Inheritance Paths in Dependent Type Theory: A Case Study in Functional Analysis
• Context Aware Calculation and Deduction
• Formal proof - the four color theorem
• Formalizing an analytic proof of the prime number theorem
• How to write mathematics
• scientific article; zbMATH DE number 5278955 (Why is no real title available?)
• scientific article; zbMATH DE number 3251317 (Why is no real title available?)
• On teaching mathematics
• The Architecture of Mathematics
• The Lean 4 theorem prover and programming language
• The Lean theorem prover (system description)
• The phenomenology of mathematical beauty
• Two simple proofs of the Kochen-Specker theorem
• Ugly mathematics: why do mathematicians dislike computer-assisted proofs?
• What is good mathematics?

Cited in

(1)

• Constructing the Lie algebra of smooth vector fields on a Lie group in Isabelle/HOL

This page was built for publication: Algorithm and abstraction in formal mathematics

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6637783)