A formal proof of the kepler conjecture

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

Forum of Mathematics, Pi（2017）

引用 182|浏览3

暂无评分

摘要

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.

查看译文

AI 理解论文

溯源树

样例

生成溯源树，研究论文发展脉络

Chat Paper

正在生成论文摘要