Formalizing (One of) the Hundred Greatest Theorems
In 1999, mathematicians 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, 99% of these theorems have been formalized on a computer, using a variety of different proof assistants.
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 (Windows/macOS/Linux)
- Useful knowledge/skills:
- Basic mathematics, first-order logic
- Contact:
- Tjark Weber
Last modified: 2023-05-03