A FORMAL PROOF OF THE KEPLER CONJECTURE. (29th May 2017)
- Record Type:
- Journal Article
- Title:
- A FORMAL PROOF OF THE KEPLER CONJECTURE. (29th May 2017)
- Main Title:
- A FORMAL PROOF OF THE KEPLER CONJECTURE
- Authors:
- 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 - Abstract:
- 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.
- Is Part Of:
- Forum of mathematics. Volume 5(2017)
- Journal:
- Forum of mathematics
- Issue:
- Volume 5(2017)
- Issue Display:
- Volume 5, Issue 2017 (2017)
- Year:
- 2017
- Volume:
- 5
- Issue:
- 2017
- Issue Sort Value:
- 2017-0005-2017-0000
- Page Start:
- Page End:
- Publication Date:
- 2017-05-29
- Subjects:
- 52C17
Mathematics -- Periodicals
510 - Journal URLs:
- http://journals.cambridge.org/action/displayJournal?jid=FMP ↗
- DOI:
- 10.1017/fmp.2017.1 ↗
- Languages:
- English
- ISSNs:
- 2050-5086
- Deposit Type:
- Legaldeposit
- View Content:
- Available online (eLD content is only available in our Reading Rooms) ↗
- Physical Locations:
- British Library HMNTS - ELD Digital store
- Ingest File:
- 144.xml