Algorithm and abstraction in formal mathematics
From MaRDI portal
Publication:6637783
DOI10.1007/978-3-031-64529-7_2MaRDI QIDQ6637783
Publication date: 13 November 2024
Cites Work
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- The phenomenology of mathematical beauty
- A verified ODE solver and the Lorenz attractor
- Ugly mathematics: why do mathematicians dislike computer-assisted proofs?
- The Lean 4 theorem prover and programming language
- Are these the most beautiful?
- How to write mathematics
- A mathematician's apology.
- Formalizing an analytic proof of the prime number theorem
- Beauty Is Not Simplicity: An Analysis of Mathematicians' Proof Appraisals
- The Lean Theorem Prover (System Description)
- Automating Elementary Number-Theoretic Proofs Using Gröbner Bases
- A Down-to-Earth View of Mathematics
- On teaching mathematics
- Two simple proofs of the Kochen-Specker theorem
- Competing Inheritance Paths in Dependent Type Theory: A Case Study in Functional Analysis
- A FORMAL PROOF OF THE KEPLER CONJECTURE
- A Machine-Checked Proof of the Odd Order Theorem
- Context Aware Calculation and Deduction
- What is good mathematics?
- The Architecture of Mathematics
- Abstraction boundaries and spec driven development in pure mathematics
- A formalization of the change of variables formula for integrals in mathlib
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)
