A FORMAL PROOF OF THE KEPLER CONJECTURE

HALES, THOMAS; ADAMS, MARK; BAUER, GERTRUD; DAT DANG, TAT; HARRISON, JOHN; TRUONG HOANG, LE; KALISZYK, CEZARY; MAGRON, VICTOR; MCLAUGHLIN, SEAN; THANG NGUYEN, TAT; TRUONG NGUYEN, QUANG; NIPKOW, TOBIAS; OBUA, STEVEN; PLESO, JOSEPH; RUTE, JASON; SOLOVYEV, ALEXEY; HOAI AN TA, THI; TRUNG TRAN, NAM; DIEP TRIEU, THI; URBAN, JOSEF; VU, KY; ZUMKELLER, ROLAND

doi:10.1017/fmp.2017.1

Public

A FORMAL PROOF OF THE KEPLER CONJECTURE

Shared by NobleBlocks on Jan 1, 2017 • 12:00 AM UTC

Authors:

THOMAS HALES

MARK ADAMS

GERTRUD BAUER

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.

Research Assistant

AI chat, annotations, notes & similar papers

Finding related papers...

Discussions

(0)

No comments yet

Be the first to share your thoughts!