Computer theorem proving in mathematics
From MaRDI portal
Publication:704001
DOI10.1007/s11005-004-0607-9zbMath1067.03020arXivmath/0311260OpenAlexW3100561060MaRDI QIDQ704001
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
Lua error in Module:PublicationMSCList at line 37: attempt to index local 'msc_result' (a nil value).
Related Items (5)
Explaining Gabriel-Zisman localization to the computer ⋮ Homotopy type theory and Voevodsky’s univalent foundations ⋮ First steps towards a formalization of forcing ⋮ Implementation of Bourbaki's Elements of Mathematics in Coq: Part Two, From Natural Numbers to Real Numbers ⋮ On the formalization of gamma function in HOL
Uses Software
Cites Work
- 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
- 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
This page was built for publication: Computer theorem proving in mathematics
