报告人: Thomas Hales (University of Pittsburgh)

时间: 2:00-3:00 pm, July 18 (Saturday) 2015

地点: Lecture Hall 501, CMS, Zhejiang University

题目: The formal proof of the Kepler conjecture

 

摘要:In 1611,Kepler asserted that no packing of congruent balls in space can have density greater than the familier cannonball arrangement.This statement known as the Kepler conjecture,is now a theorem that has been formally verified.A theorem is formally verified if every step of the proof has been checked at the level of the primitive inference rules of logic and the foundational axioms of mathematics.This talk will present the Kepler conjecture,Its proof,and background about the formal verification of theorems.

 

Hales教授介绍

 

Thomas Hales教授现任美国匹兹堡大学数学系Andrew Mellon讲座教授。他在1986年师从数学大师Robert Langlands获得普林斯顿大学博士学位。先后任教于哈佛大学（1987-1989），普林斯顿高等研究院（1989-1990），芝加哥大学（1990-1993），密歇根大学（1993-2001），匹兹堡大学（2001-）等。

 

Hale教授在数论基本引理方面做了许多开创性的工作。数论基本引理被越南数学家吴宝珠（2010年菲尔兹奖获得者）在2008年证明，他用到了Hales引入的许多想法。Hales教授在1988年证明了有着数百年历史的关于球堆体积最优密度的开普勒猜想。最近他用计算机形式化验证了他的证明。他的工作开创了计算机用于复杂数学证明的新机制。