Second International Workshop on Formal Proof and the Flyspeck Project

Schedule

Workshop info in Vietnamese

News

• How to install HOL Light on Windows

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.

The workshop in 2009 supplied training in methods of formal proof. Significant training is required to make meaningful contributions to a formalization project. This workshop will gather together experts in formal proof, with the purpose of working together to further the Flyspeck project. 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 participants will be expected to have a background in OCaml, theorem proving in HOL Light, methods of real analysis, discrete geometry, and the proof of the Kepler conjecture. 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.

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 and the Benter Foundation.