Computer theorem proving in mathematics

DOI10.1007/s11005-004-0607-9zbMath1067.03020arXivmath/0311260MaRDI QIDQ704001

Carlos T. Simpson

Publication date: 12 January 2005

Published in: Letters in Mathematical Physics (Search for Journal in Brave)

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

zbMATH Keywords

verification; theorem proving; set theory; type theory; Lambda calculus

Mathematics Subject Classification ID

03B35: Mechanization of proofs and logical operations

68-02: Research exposition (monographs, survey articles) pertaining to computer science

Related Items

Explaining Gabriel-Zisman localization to the computer

Uses Software

• ACL2
• Coq
• TPS
• Isar
• Mizar
• LCF
• Flyspeck

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Two models of synthetic domain theory
• Algebraic geometry in first-order logic
• Hodge cycles, motives, and Shimura varieties
• A mechanical proof of quadratic reciprocity
• A mechanical proof of the termination of Takeuchi's function
• Finite functions and the necessary use of large cardinals
• Homotopy hyperbolic 3-manifolds are hyperbolic
• A counterexample to a 1961 ``theorem in homological algebra
• A comparison of Mizar and Isar
• Vanquishing the XCB question: The methodological discovery of the last shortest single axiom for the equivalential calculus
• A Ramsey theorem in Boyer-Moore logic
• Computer proofs of limit theorems
• STRINGS AND BRANES IN NON-ABELIAN GAUGE THEORY
• The Non-Existence of Finite Projective Planes of Order 10
• Recursive functions of symbolic expressions and their computation by machine, Part I
• (In)consistency of Extensions of Higher Order Logic and Type Theory
• On Lipschitz Homogeneity of the Hilbert Cube
• A mechanical proof of the Church-Rosser theorem
• Studies in Duality on Noetherian Formal Schemes and Non-Noetherian Ordinary Schemes
• Theorem-Proving on the Computer
• Metamathematics, Machines and Gödel's Proof
• A Machine-Oriented Logic Based on the Resolution Principle
• The nonexistence of ovals in a projective plane of order 10