A FORMAL PROOF OF THE KEPLER CONJECTURE

Hales, Thomas; ADAMS, MARK; BAUER, GERTRUD; DANG, TAT DAT; HARRISON, JOHN; HOANG, LE TRUONG; Kaliszyk, Cezary; MAGRON, VICTOR; McLaughlin, Sean; NGUYEN, TAT THANG; NGUYEN, QUANG TRUONG; NIPKOW, TOBIAS; OBUA, STEVEN; PLESO, JOSEPH; RUTE, JASON; Solovyev, Alexey; TA, THI HOAI AN; TRAN, NAM TRUNG; TRIEU, THI DIEP; URBAN, JOSEF; VU, KY; ZUMKELLER, ROLAND

doi:10.1017/fmp.2017.1

Record: found
Abstract: found
Article: found

Is Open Access

A FORMAL PROOF OF THE KEPLER CONJECTURE

Author(s): 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

Publication date (Print): May 2017

Journal: Forum of Mathematics, Pi

Publisher: Cambridge University Press (CUP)

Read this article at

ScienceOpen Publisher

Bookmark

There is no author summary for this article yet. Authors can add summaries to their articles on ScienceOpen to make them more accessible to a non-specialist audience.

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.