Interactive theorem provers are tools that help mathematicians write proofs.

Today, they are not yet ready to be used by research mathematicians, but that day may come soon! The dream is that these tools will extend the power and reach of human mathematicians.

In a project on interactive theorem proving you might:

• Learn how to write and verify proofs using software tools.
• Develop the library of mathematics understood by a modern theorem prover.
• Build pedagogical tools to help students learn to write careful proofs.
• Study the software engineering aspects of building massive libraries of mathematical theories, that are modular and reusable.
• Develop "tactics", namely algorithms that help write proofs, either in the form of decision procedures for particular problems, or general heuristics, possibly involving machine learning, for broad classes of mathematical problems.
• Get a head-start in the new world of computer-assisted mathematics.

This project will use the new interactive theorem prover Lean.

Previous background required:

• Experience writing careful and detailed proofs.
• Experience in a strongly typed functional language, e.g. Haskell, or perhaps Scala, is very helpful.

Suggested reading:

• Getting started with Lean
• Theorem proving in Lean
• The mathematical library for Lean
• Certified programming with dependent types