The Flyspeck Project

final result です．

# tame_nonlinear_imp_kepler_conjecture;;
val it : thm =
  |- import_tame_classification /\ the_nonlinear_inequalities
     ==> the_kepler_conjecture

# SIMP_RULE [the_kepler_conjecture_def; import_tame_classification; the_nonlinear_inequalities] it;;
val it : thm =
  |- (!g. PlaneGraphs g /\ tame g
          ==> (?y. y IN archive /\ iso_fgraph (fgraph g) y)) /\
     pack_nonlinear_non_ox3q1h /\
     ox3q1h /\
     main_nonlinear_terminal_v11 /\
     lp_ineqs /\
     pack_ineq_def_a /\
     kcblrqc_ineq_def
     ==> (!V. packing V
              ==> (?c. !r. &1 <= r
                           ==> &(CARD (V INTER ball (vec 0,r))) <=
                               pi * r pow 3 / sqrt (&18) + c * r pow 2))