A FORMAL PROOF OF THE KEPLER CONJECTURE
Copyright policy )A FORMAL PROOF OF THE KEPLER CONJECTURE
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.
- Chinese University of Hong Kong China (People's Republic of)
- Radboud University Nijmegen Netherlands
- Pennsylvania State University United States
- Technical University of Munich Germany
- Institute of Mathematics Viet Nam
FOS: Computer and information sciences, Computer Science - Logic in Computer Science, HOL Light proof assistant, cs.LO, Mathematics - Metric Geometry, formal proof, QA1-939, FOS: Mathematics, HOL, Packing and covering in \(n\) dimensions (aspects of discrete geometry), math.MG, Data Science, Metric Geometry (math.MG), Isabelle proof assistant, 004, Logic in Computer Science (cs.LO), ball packing, Kepler conjecture, 52C17, Flyspeck project, Mathematics, Theorem proving (deduction, resolution, etc.)
FOS: Computer and information sciences, Computer Science - Logic in Computer Science, HOL Light proof assistant, cs.LO, Mathematics - Metric Geometry, formal proof, QA1-939, FOS: Mathematics, HOL, Packing and covering in \(n\) dimensions (aspects of discrete geometry), math.MG, Data Science, Metric Geometry (math.MG), Isabelle proof assistant, 004, Logic in Computer Science (cs.LO), ball packing, Kepler conjecture, 52C17, Flyspeck project, Mathematics, Theorem proving (deduction, resolution, etc.)
selected citations These citations are derived from selected sources.This is an alternative to the "Influence" indicator, which also reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically).215 popularity This indicator reflects the "current" impact/attention (the "hype") of an article in the research community at large, based on the underlying citation network.Top 1% influence This indicator reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically).Top 1% impulse This indicator reflects the initial momentum of an article directly after its publication, based on the underlying citation network.Top 1%
Citations provided by BIP!Popularity provided by BIP!