BSc/MSci projects

I'm happy to supervise all interesting projects, but I have most to contribute for projects involving formal methods, programming languages, AI for theorem proving, and the mathematical foundations of computing. Some projects involve building software, while other involve proving things either on paper or in a proof assistant. The proposals below are indicative starting points and not a fixed menu. If you have an idea of your own that connects to these areas, please get in touch: I would be happy to work out a suitable project with you.

BSc students will have seen some Lean in IFR. That's enough background to consider the Lean projects; you don't need to be an expert already. The AI and Data Science projects don't require Lean.

Depending on the question, we might instead use Agda, Python, Haskell, another language, or pen and paper. We would agree on a manageable core project and possible extensions together.

Some concrete project proposals

Can an small AI agent prove theorems in Lean or Agda?

Build a small agent (using local or free models) that proposes proof steps, asks Lean whether they work, and uses the feedback to try again. Compare a few approaches, for example, giving the agent relevant lemmas, allowing it to backtrack, or breaking a proof into smaller goals, on a fixed collection of problems. The dissertation would analyse which problems it solves, where it fails, and what the Lean checker contributes. A good project does not depend on training a new language model or obtaining expensive hardware or subscriptions. Especially suitable for CS+AI, with a substantial formal-reasoning component.

Prove a pathfinding algorithm correct

Implement breadth-first search or a version of Dijkstra's algorithm, and prove a correctness theorem, for instance, that a returned path is valid and has minimum length under suitable assumptions. Start with a simple representation of graphs and add efficiency improvements as time permits. You can compare the verified program with ordinary testing and explain what each approach establishes. This is a route into software verification through a familiar algorithm.

Design a tiny programming language and prove something about it

Define a small language of program expressions with an interpreter and type checker. Then prove a theorem such as “a well-typed program does not get stuck.” There is room to choose the language: a small imperative or functional language, or a restricted language for describing a particular kind of computation. The initial language should be deliberately small with features such as first-class functions or mutable state as extensions. The outcome is a working implementation and a clearly stated, checked correctness argument.

Build a quantum puzzle with a reliable simulator

Design a small puzzle or game in which players apply quantum gates and measurements to a few qubits. Build the simulator, make the rules understandable to players, and test its behaviour against independently calculated examples. You could then investigate puzzle design or how to explain the quantum state to a player. A larger game building in elements of common quantum algorithms is a possible extension, but a small, well-evaluated puzzle is already a worthwhile dissertation.

Calculate with exact real numbers

Build a small library that can represent exact real numbers, either via increasingly accurate approximations, narrowing intervals, or other increasing amounts of information. Investigate which operations it supports and how it performs on carefully chosen examples. The project could be mainly programming, or could include proofs of correctness. This is a more mathematical option for students interested in the connection between computation, logic, and topology.

When does topology help classify time series?

Topological Data Analysis looks at geometric features of data sets (loops and higher-dimensions “holes”) that persist as the scale of observation changes. Take a small selection of time-series classification problems, turn each series into a point cloud using a time-delay embedding, and compute persistent-homology features with an existing Python package such as Ripser. Compare a simple classifier using TDA with a sensible baseline to investigate when the topological features help, when they fail, and why. (This could be suitable for a Data Science project.)