Theorem Proving in Higher Order Logics

DOI10.1007/B100400MaRDI QIDQ5464666zbMATH OpenOpenAlexFDO

Authors Thomas C. Hales

Publication date 18 August 2005

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/b100400

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Packing and covering in (n) dimensions (aspects of discrete geometry) (52C17)

Recommendations

• A formal proof of the Kepler conjecture
• A formulation of the Kepler conjecture
• Linear Programs for the Kepler Conjecture
• The Kepler Conjecture
• scientific article; zbMATH DE number 1789934

Cited in

(16)

• Ten methods to bound multiple roots of polynomials
• A replication crisis in mathematics?
• Sphere packings revisited
• A mathematical proof proved correct: the most efficient way to pack spheres
• Floating-point arithmetic on the test bench. How are verified numerical solutions calculated?
• Type inference for ZFH
• Combined Decision Techniques for the Existential Theory of the Reals
• scientific article; zbMATH DE number 1789934 (Why is no real title available?)
• ON A STRONG VERSION OF THE KEPLER CONJECTURE
• Proof auditing formalised mathematics
• A formal proof of the Kepler conjecture
• scientific article; zbMATH DE number 2209729 (Why is no real title available?)
• scientific article; zbMATH DE number 2237875 (Why is no real title available?)
• Historical overview of the Kepler conjecture
• An intuitionistic proof of a discrete form of the Jordan curve theorem formalized in Coq with combinatorial hypermaps
• A revision of the proof of the Kepler conjecture

Describes a project that uses

Uses Software

• kepler98

This page was built for publication: Theorem Proving in Higher Order Logics

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