Back to Search
Start Over
A FORMAL PROOF OF THE KEPLER CONJECTURE
- Source :
- Forum of Mathematics. Pi, 5, 1-29, Forum of Mathematics. Pi, 5, pp. 1-29, Forum of Mathematics, Pi
- Publication Year :
- 2017
-
Abstract
- This article describes a formal proof of the Kepler conjecture on dense sphere packings in a combination of the HOL Light and Isabelle proof assistants. This paper constitutes the official published account of the now completed Flyspeck project.<br />21 pages
- Subjects :
- FOS: Computer and information sciences
Statistics and Probability
Computer Science - Logic in Computer Science
0102 computer and information sciences
01 natural sciences
Formal proof
Kepler conjecture
symbols.namesake
Mathematics - Metric Geometry
FOS: Mathematics
Hol light
Discrete Mathematics and Combinatorics
0101 mathematics
GeneralLiterature_REFERENCE(e.g.,dictionaries,encyclopedias,glossaries)
Mathematical Physics
Mathematics
Algebra and Number Theory
010102 general mathematics
Data Science
Metric Geometry (math.MG)
Logic in Computer Science (cs.LO)
Algebra
010201 computation theory & mathematics
symbols
Geometry and Topology
Analysis
Subjects
Details
- ISSN :
- 20505086
- Volume :
- 5
- Database :
- OpenAIRE
- Journal :
- Forum of Mathematics. Pi
- Accession number :
- edsair.doi.dedup.....a280db53ee95a279e1aa5fc6830335ea