Home Page
Workshop on Formal Proof and the Flyspeck Project
| Duration: | June 8 - July 31, 2009 |
| Organizer: | Thomas Hales |
| Location: | Hanoi Institute of Mathematics 18 Hoàng Quốc Việt, CauGiay District, Hanoi, Vietnam [map] [photo] |
News
Goals of the workshop
A formal proof is a proof in which every logical inference has been checked at the most basic foundational level of mathematics. By contrast, conventional proofs are made at a much higher level. Because of the number of steps involved, computers are generally used to make a formal proof. Researchers working in the area of formal proofs need training in both mathematics and in the formal proof software.
One of the major goals of this workshop will be to supply further training in methods of formal proof. Significant training is required to make meaningful contributions to a formalization project. This workshop will train beginners who are learning the methods of formal proof for the first time. It will give advanced training to researchers who already know how to construct formal proofs on computer.
The Flyspeck project is one of the largest formal proof projects ever attempted. Its purpose is to give a formal proof of the Kepler conjecture on sphere packings. The workshop will bring together different researchers involved in the Flyspeck project. The workshop will also provide training for the Flyspeck formal proof project.
The training topics will include programming in OCaml, theorem proving in HOL Light, methods of real analysis, discrete geometry, and the proof of the Kepler conjecture. Interaction among Western and Vietnamese members of the research project will be especially encouraged. The workshop will provide advanced members of the research project opportunities to discuss and develop new approaches to formalization, and to collaborate on the Flyspeck project. The workshop will to provide additional training in methods of formal proof at all levels.
About Hanoi for Foreign Participants
Basic facts about travel are available from Frommer's page on Hanoi. Vietnam has opened itself to Western visitors in a major way over the past several years. Visas are generally required. Multiple entry visas are suggested for participants who are considering any travel to neighboring countries.
Registration
Please contact Thomas Hales for further details. Those wishing to participate should register for the workshop by sending an email to Thomas Hales.
This workshop is supported by funding from the National Science Foundation, grant 0804189.