2014-11-17から1日間の記事一覧
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_nonli…