Introduction

The text part of the formalization project is now nearly complete. The following individuals have contributed lemmas to the text project:

• Dang Tat Dat
• Hales, Thomas C.
• Harrison, John
• Hoang Le Truong
• Nguyen Tat Thang
• Nguyen Quang Truong
• Rute, Jason
• Solovyev, Alexey
• Thi Trieu Diep
• Tran Nam Trung
• Vu Khac Ky
• Vu Thanh
• Vuong Anh Quyen

(Numerous others have made contributions to the code project.)

The Last 32 Pages

As of June 23, 2011, there were 32 pages left of the text formalization project. This page tracks is the status of these final pages. LP=lines of proof in the English text (488 total).

• Lines left
• 488 (June 23 2011)
• 367 (Jan 28 2012)
• 295 (May 15 2012)

• Hypermap Chapter (0 pages)
• CTJYKFZ (8 LP) -- added 5/3/2012

• Fan Chapter (0 pages)
• JLIGZGS (14 LP)
• AMHFNXP (26 LP) -- HLT 7/30/2011
• WBLARHH (3 LP) -- HLT 7/30/2011
• BSXAQBQ (1 LP) -- HLT 7/30/2011
• FLVNSME (15 LP) -- HLT 7/30/2011
• CFYXFTY (30 LP) -- overlooked in June estimate -- HLT 3/5/2012

• Packing Chapter (19 pages, 191 LP)
• DUUNHOR (28 LP) --overlooked in June estimate-- Solovyev 8/2011
• SLTSTLO (12 LP) -- VKK 7/2011
• RVFXZBU (14 LP)-- VKK 12/2011
• URRPHBZ (2 LP)-- VKK 12/2011
• QZYZMJC (1 LP)-- VKK 1/12/2012
• GRUTOTI (10 LP)-- VKK 3/14/2012
• KIZHLTL (26 LP)-- VKK 5/10/2012
• TSKAJXY (1 LP -- computer calculation) -- VKK
• OXLZLEZ (7 LP)
• UPFZBZM (16 LP) -- VKK 5/15/2012
• RDWKARC (5 LP) -- VKK 5/15/2012
• EUSOTYP (23 LP) --TCH 2/7/2012
• GOTCJAH (30 LP) -- TCH
• DLWCHEM (30 LP) -- TCH
• XULJEPR (14 LP) -- TCH

• Packing Chapter (added Dec 2011 to show that Marchal cells partition space)
• HDTFNFZ (8 LP)-- VKK 12/2011
• NJIUTIU (10 LP)-- VKK 12/31/2011
• TEZFFSK (11 LP)-- VKK 12/31/2011
• YNHYJIT (9 LP)-- VKK 12/31/2011
• QZKSYKG (7 LP)-- VKK 1/9/2012
• DDZUPHJ (15 LP)-- VKK 1/9/2012
• AJRIPQN (9 LP)-- VKK 1/9/2012

• Local Fan Chapter (8 pages, 172 LP)
• EGHNAVX (26 LP)
• XRECQNS (15 LP) -- NQT
• MHAEYJN (46 LP) -- NQT
• ZLZTHIC (proof combined with previous lemma) --NQT
• EJRCFJD (17 LP) -- NQT
• NKEZBFC (7 LP) -- HLT 8/2011
• BGMIFTE (36 LP) -- JH
• WSEWPCH (25 LP) -- JH

• Tame Hypermap Chapter (2 pages, 66 LP)
• FNJLBXS (35 LP) -- AS
• FCDJDOT (10 LP) -- AS
• KCBLRQC (21 LP) -- AS

The Fine Print

• The 32 pages does not include the parts of the text (such as remarks, introductory passages, and auxiliary results) that are not strictly a part of the proof of the Kepler conjecture.
• It does not include the parts of the Kepler conjecture that lie outside the text. That is, it does not include the computer portions of the proof.
• Also excluded are three specific sections of the text that talk about the relationship between the text and the computer portions of the proof.
• The last chapter of the book, on the strong dodecahedral conjecture and Fejes Toth's contact conjecture, are excluded.