Pith. sign in

REVIEW 1 cited by

A formal proof of the Kepler conjecture

Not yet reviewed by Pith; the record is open.

Re-run · record.json Download PDF Read on arXiv ↗

This paper has not been read by Pith yet. Machine review is queued; the pith claim, tier, and objections will appear here once it completes.

SPECIMEN: schema-true, not a live event

T0 review · schema-true

One-sentence machine reading of the paper's core claim.

pith:XXXXXXXX · record.json · timestamp

arxiv 1501.02155 v1 pith:OL7XNF2Q submitted 2015-01-09 math.MG cs.LO

A formal proof of the Kepler conjecture

Thomas Hales , Mark Adams , Gertrud Bauer , Dat Tat Dang , John Harrison , Truong Le Hoang , Cezary Kaliszyk , Victor Magron
show 14 more authors
Sean McLaughlin Thang Tat Nguyen Truong Quang Nguyen Tobias Nipkow Steven Obua Joseph Pleso Jason Rute Alexey Solovyev An Hoai Thi Ta Trung Nam Tran Diep Thi Trieu Josef Urban Ky Khac Vu Roland Zumkeller
This is my paper
classification math.MG cs.LO
keywords proofconjectureformalkepleraccountarticleassistantscombination
verification ladder T0 review T1 audit T2 compute T3 formal T4 reserved
0 comments
read the original 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.

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Forward citations

Cited by 1 Pith paper

Reviewed papers in the Pith corpus that reference this work. Sorted by Pith novelty score.

  1. Theory-Level Autoformalization: From Isolated Statements to Unified Formal Knowledge Bases

    cs.AI 2026-07 conditional novelty 5.0

    Autoformalization should target complete theories—axioms, definitions, lemmas, proofs—as unified formal libraries, not isolated statements.