| Autor: |
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 |
| Jazyk: |
angličtina |
| Rok vydání: |
2017 |
| Předmět: |
|
| Zdroj: |
Forum of Mathematics, Pi, Vol 5 (2017) |
| Druh dokumentu: |
article |
| ISSN: |
2050-5086 |
| DOI: |
10.1017/fmp.2017.1 |
| Popis: |
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. |
| Databáze: |
Directory of Open Access Journals |
| Externí odkaz: |
|
