Automated reasoning for mathematics

DOI10.1007/978-3-031-63498-7_1MaRDI QIDQ7034882zbMATH OpenFDO

Authors Jeremy Avigad

Publication date 31 January 2025

Copyright license Creative Commons Attribution 4.0 International

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

Mathematics Subject Classification ID

Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Cites work

• scientific article; zbMATH DE number 3950473 (Why is no real title available?)
• scientific article; zbMATH DE number 3487395 (Why is no real title available?)
• scientific article; zbMATH DE number 1543300 (Why is no real title available?)
• scientific article; zbMATH DE number 2123258 (Why is no real title available?)
• scientific article; zbMATH DE number 7350778 (Why is no real title available?)
• A formally verified proof of the central limit theorem
• A formally verified proof of the prime number theorem
• A machine-checked proof of the odd order theorem
• A unification algorithm for typed \(\bar\lambda\)-calculus
• Alan Turing: Life and Legacy of a Great Thinker
• An extensible user interface for Lean 4
• Automated theorem proving in quasigroup and loop theory
• Backtrack Programming
• Certified knowledge compilation with application to verified model counting
• Decision algorithms for Fibonacci-automatic words. I: Basic results.
• Empty convex hexagons in planar point sets
• Extending a high-performance prover to higher-order logic
• Formal proof - the four color theorem
• Formal verification of the empty hexagon number
• Homotopy limits in type theory
• Machine-learned premise selection for Lean
• Nitpick: a counterexample generator for higher-order logic based on a relational model finder
• Opinion: The Mechanization of Mathematics
• Practical Proof Search for Coq by Type Inhabitation
• Solution of the Robbins problem
• Superposition for higher-order logic
• Term rewriting and beyond -- theorem proving in Isabelle
• The Jordan Curve Theorem, Formally and Informally
• The Lean 4 theorem prover and programming language
• The Lean theorem prover (system description)
• The Logical Approach to Automatic Sequences
• The automation of proof: a historical and sociological exploration
• The classical decision problem.
• The empty hexagon theorem
• Types for Proofs and Programs
• Über formal unentscheidbare Sätze der Principia Mathematica und verwandter Systeme. I.

Cited in

(2)

• Artificial intelligence and inherent mathematical difficulty
• Notes on Gödel's and Scott's variants of the ontological argument

This page was built for publication: Automated reasoning for mathematics

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