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 proofs; sphere packing; Kepler conjecture

Mathematics Subject Classification ID

01A65: Development of contemporary mathematics

03B35: Mechanization of proofs and logical operations

52C17: Packing and covering in (n) dimensions (aspects of discrete geometry)

05B40: Combinatorial aspects of packing and covering

Uses Software

• Coq
• NQTHM
• Flyspeck