Here is a list of projects in the area of formal mathematics that I consider worthwile. It can be used as a source for master's projects. The projects are not explained. In case you are interested in a description of one of these projects, mail me at freek@cs.kun.nl.

For each of the projects I added an estimate of how difficult I think it might be. I have no idea how accurate these estimates are. The idea is that a project of "1 week-1 month" would be suitable for a master's project. Part of a project of "1 month-1 year" could be a master's project as well, or the whole project could be part of a Ph.D. project. A project of "1 year-10 years" could be a Ph.D. project.

The list is divided in categories following the classification of research in this area that Christine Paulin made during the evaluation session at the end of the TYPES workshop in Kloster Irsee in 1998. I added a fourth category, "Knowledge Management", because the last project didn't fit any of her three categories.

1. Formalize Euclid. [1 year-10 years]

   Stages: Tarski's axioms to Euclid's axioms, Tarski's axioms to "betweenness axioms", Euclid's axioms + "betweenness axioms" to Euclid. Try to be faithful to the original.

2. Formalize Euler's formula. [1 month-1 year]

   Try to be faithful to definitions from Proofs and Refutations.

3. Formalize the game of Hex constructively and extract a winning strategy. [1 week-1 month]

4. Formalize Conway's theory of numbers and games. [1 week-1 month]

   Use this to define the real numbers. (This was done in Coq by Lionel Mamane.)

5. Formalize the proof of the Jordan curve theorem from algebraic topology. [1 month-1 year]

6. Formalize the snake lemma from algebraic topology. [1 week-1 month]

   Trivial but fun!

7. Formalize spaces from Counterexamples in Topology. [1 month-1 year]

   The Tychonoff corkscrew!

8. Formalize Shostak's algorithm using reflection. [1 month-1 year]

   (This is one of Gilles Dowek's master thesis problems.)

9. Formalize a proof of the four color theorem. [1 year-10 years]

   (This is the project of George Gonthier and Benjamin Werner.)

10. Formalize the semantics of a subset of the expressions of Maple or Mathematica. [1 month-1 year]

    Deal with: undefinedness, infinity, constants of integration, big-Oh notation.

11. Formalize the prime number theorem. [1 year-10 years]

    (This is Bob Solovay's challenge.)

1. Implement a real time incremental checker for a declarative proof language. [1 month-1 year]

   Color the text lines in an editor according to current status: comment (blue), unchecked (gray), incorrect (red), correct but refers to incorrect lines (brown), correct and only refers to correct lines (black).

2. Implement a proof general interface for HOL Light. [1 month-1 year]

3. Implement a translator from Mathpert calculations to formal proofs. [1 month-1 year]

4. Implement a geometry proof tool that represents the context in a diagram. [1 month-1 year]

   Find a way to represent inconsistent statements. Find a way to prove things graphically in Hyperproof style. Generalize this to a graph theory proof tool. Generalize this to a commuting diagram proof tool.

5. Implement a prover in which tactic scripts and proof terms are the same thing. [1 week-1 month]

   Make it satisfy the de Bruijn principle.

6. Implement a translator from resolution proofs to natural deduction. [1 month-1 year]

   (This is part of Dimitri Hendriks' Ph.D. project.)

7. Implement a proof disassembler. [1 month-1 year]

   Like "relinfer" but with an arbitrary prover. Find out how to deal with changing contexts,

8. Implement a translator from Mizar to untyped set theory in first order logic. [1 month-1 year]

   Let it be a de Bruijn checker for Mizar. (This is the project of Joseph Urban.)

9. Implement a folding interface to Mizar. [1 month-1 year]

   Fold away: labels/justifications, intermediate steps, subproofs. Have expressions both in ascii style and in formula style. Alongside: an abstract, a proof sketch, the full formalization.

10. Implement a proof sketch extractor for Mizar. [1 month-1 year]

    Part of the previous. Not interactive.

1. Develop a theory of the relation between pi-typed and lambda-typed type theory. [1 month-1 year]

2. Develop a theory of the relation between ZFC in FOL and ZFC in HOL. [1 month-1 year]

3. Develop a theory of higher order logic with domain conditions. [1 month-1 year]

4. Develop a theory of sets of lambda terms as directed graphs. [1 month-1 year]

5. Develop a theory of hierarchical reflection. [1 week-1 month]

   (This is being worked on by Luís Cruz-Filipe.)

1. Select twelve textbooks for the twelve undergraduate math subjects. [1 week-1 month]

   Select them to go together well. Present a list of alternatives for each subject.

(last modification 2002-01-31)