Kapler填球猜想证明始末
(转载)
kapler 猜想是说:正方体内装满同样的小球,小球的体积与长方体体积的比不会大于π/√18(约为74%)。首先由kapler于1611年提出。
这个问题的困难在于目前的想法都要涉及到大量的枚举,所以都感到很难下手,这要归结于1953年 匈牙利数学家Fejes Toth的创造性想法。
随后英国数学家Claude Ambrose Rogers1958年提出至少那个比不会大于78%,但是指出其方法并不能推广到证明原猜想的程度。
接下来,美籍华裔数学家项武义1993公布了一个预印本,声称采用几何途径证明了猜想,但遭到许多人的质疑,其中就有Toth认为,其中许多命题的证明不可接受。
虽然1995,2001年武义曾对质疑有所回答,主流意见仍然是猜想仍是公开问题。
值得注意的是,这时涌现了反项的急先锋 Hales ,他对项的证明的批评最为切中要害。
正是Hales,于1998年宣布了获得一个kapler猜想的的计算机辅助证明,经过12个人的团队审查,得出了“人工推理部分正确,所有 证明99%正确”的结论,经过修改和再审,终于于2005年发表于著名的Annal of Math. 这可以称作是自计算机辅助证明四色猜想以后的又一计算机辅助数学证明的奇迹,Ann. of Math. 为此还修改了投稿办法,其中就是涉及计算机辅助证明的。
但是对于Hales的证明是有争议的,其中就是计算机辅助那一部分证明的正确性,为此Hales本人发起了一项大规模合作研究计划:Project FlysPecK - the F, P and K standing for Formal Proof of Kepler,目的是给出一个人工正式证明。但是他本人估计,完成也需要约20年。
因为篇幅所限,论文的pdf文件不能上传。
注意:这个问题的复杂性由论文的篇幅可见一斑。项武义的论文100多页,Hales的论文即使采用了计算机辅助计算,其手工部分仍然长达120多页。