Interactive and automated theorem proving

The moment when research mathematicians need to pay attention to progress in automated theorem proving is coming closer and closer!

school Student intake
This project is open for Bachelor, Honours and Masters students.
group Group
traffic Project status

Project status


Content navigation


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: