Forum of Mathematics, Pi (Jan 2017)
A FORMAL PROOF OF THE KEPLER CONJECTURE
- THOMAS HALES,
- MARK ADAMS,
- GERTRUD BAUER,
- TAT DAT DANG,
- JOHN HARRISON,
- LE TRUONG HOANG,
- CEZARY KALISZYK,
- VICTOR MAGRON,
- SEAN MCLAUGHLIN,
- TAT THANG NGUYEN,
- QUANG TRUONG NGUYEN,
- TOBIAS NIPKOW,
- STEVEN OBUA,
- JOSEPH PLESO,
- JASON RUTE,
- ALEXEY SOLOVYEV,
- THI HOAI AN TA,
- NAM TRUNG TRAN,
- THI DIEP TRIEU,
- JOSEF URBAN,
- KY VU,
- ROLAND ZUMKELLER
Affiliations
- THOMAS HALES
- University of Pittsburgh, USA; ,
- MARK ADAMS
- Proof Technologies Ltd, UK Radboud University, Nijmegen, The Netherlands;
- GERTRUD BAUER
- ESG – Elektroniksystem- und Logistik-GmbH, Germany;
- TAT DAT DANG
- CanberraWeb, 5/47-49 Vicars St, Mitchell ACT 2911, Australia;
- JOHN HARRISON
- Intel Corporation, USA;
- LE TRUONG HOANG
- Institute of Mathematics, Vietnam Academy of Science and Technology, Vietnam; , , ,
- CEZARY KALISZYK
- University of Innsbruck, Austria;
- VICTOR MAGRON
- CNRS VERIMAG, France;
- SEAN MCLAUGHLIN
- Amazon, USA;
- TAT THANG NGUYEN
- Institute of Mathematics, Vietnam Academy of Science and Technology, Vietnam; , , ,
- QUANG TRUONG NGUYEN
- University of Pittsburgh, USA; ,
- TOBIAS NIPKOW
- Technische Universität München, Germany;
- STEVEN OBUA
- University of Edinburgh, UK;
- JOSEPH PLESO
- Philips Electronics North America Corporation – Andover, MA, USA;
- JASON RUTE
- The Pennsylvania State University, USA;
- ALEXEY SOLOVYEV
- University of Utah, USA;
- THI HOAI AN TA
- Institute of Mathematics, Vietnam Academy of Science and Technology, Vietnam; , , ,
- NAM TRUNG TRAN
- Institute of Mathematics, Vietnam Academy of Science and Technology, Vietnam; , , ,
- THI DIEP TRIEU
- AXA China Region Insurance Company Limited, Hong Kong;
- JOSEF URBAN
- Czech Institute of Informatics, Robotics and Cybernetics (CIIRC), Czech Republic;
- KY VU
- Chinese University of Hong Kong, Hong Kong;
- ROLAND ZUMKELLER
- DOI
- https://doi.org/10.1017/fmp.2017.1
- Journal volume & issue
-
Vol. 5
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.
Keywords
