Formalizing (One of) the Hundred Greatest Theorems

Mathematicians have compiled a list of "The Hundred Greatest Theorems," based on "the place the theorem holds in the literature, the quality of the proof, and the unexpectedness of the result." As of today, 88% of these theorems have been formalized on a computer.

Do you want to help make this 100%? Pick a theorem from your favourite area of mathematics and prove it using the interactive proof assistant Isabelle!

This project will allow you to become familiar with Isabelle, one of the world's leading software tools to assist with the development of formal proofs.

Work environment:
Isabelle (Linux, Windows (via Cygwin) or Mac)
Required knowledge/skills:
Basic mathematics, first-order logic
Tjark Weber

Last modified: 2013-03-02