From Kepler to Hales, and back to Hilbert

zbMath1270.01014MaRDI QIDQ1946041

Michael Joswig

Publication date: 17 April 2013

Published in: Documenta Mathematica (Search for Journal in Brave)

Full work available at URL: http://www.emis.de/journals/DMJDMV/vol-ismp/62_joswig-michael.html

zbMATH Keywords

formal proofssphere packingKepler conjecture

Mathematics Subject Classification ID

Development of contemporary mathematics (01A65) Mechanization of proofs and logical operations (03B35) Packing and covering in (n) dimensions (aspects of discrete geometry) (52C17) Combinatorial aspects of packing and covering (05B40)

Uses Software

• Coq
• NQTHM
• Flyspeck