Skip to main content

Maximilian Doré

Personal photo - Maximilian Doré

Maximilian Doré

Departmental Lecturer

College Lecturer, Corpus Christi College
College Lecturer, Merton College

E: firstname.lastname@cs.ox.ac.uk (without accent)

Room 415, Wolfson Building, Parks Road, Oxford OX1 3QD
United Kingdom

Interests

My main research interest is in formalised mathematics, which is the project of encoding mathematics in a way that it can be understood by a computer. Provided this works, we can use computers to check the correctness of mathematical work, and to explore theories and derive proofs automatically. However, it turns out that it's already challenging to devise a language that is appropriate to express modern mathematics. One proposal for such a language is dependent type theory, which moreoever has the nice property of being a programming language. I'm interested in leveraging this dual character to provide new tools for computational mathematics on the one hand, and the mathematical foundations of programming on the other hand.

As a departmental lecturer, I'm involved with running several courses. I'm also a college lecturer at Corpus Christi and Merton, where I frequently teach Functional Programming, Models of Computation, Introduction to Proof Systems and Algorithms and Data Structures.

If you want to work with me, or do a student project, please get in touch! I'm always interested to explore new topics in interactive/automated theorem proving, programming languages, and logic in general.

Current Projects

Proof search in Cubical Type Theory

with Anders Mörtberg and Evan Cavallo

Cubical type theory, as implemented, e.g., in Cubical Agda, takes certain properties of (abstract models of) topological spaces and makes them into principles of logic. One such principle is Kan filling, we study it from the point of view of automated reasoning and develop a solver which can construct many useful applications of Kan filling.

Relevant Publications:

2024, FSCD: MD, Evan Cavallo and Anders Mörtberg, Automating Boundary Filling in Cubical Agda

Topological Data Analysis in Cubical Agda

This project is concerned with formalising discrete Morse theory, a central method in topological data analysis, in Cubical Agda. Based on this, I hope to eventually provide a tool for topological data analysis which is fully formalised.

Relevant Publications:

2024, DPhil thesis: Computing Spaces in Type Theory, University of Oxford.

Learning to write Agda with Hindsight Experience Replay

with Michael Rawson

In Agda, theorems are proved by forward reasoning, i.e., by explicitly constructing proof terms. This, and the lack of training data, makes it a good training objective for hindsight experience replay, a machine learning technique where the model constructs arbitrary proof terms and afterwards pretends the thereby established theorem was the problem to be solved. We explore how Hindsight can be used to provide a model that generates Agda proofs.

Relevant Publications:

2024, AITP: Michael Rawson, Zsolt Zombori, MD and Christoph Wernhard, Project Proposal: Forward Reasoning in Hindsight

Past Projects

Interactive theorem proving for undergraduate students

with Krysia Broda

We provide the theorem prover Elfe as a tool for undergraduate students to learn mathematical reasoning. The prover aims to bridge the gap between informal and formal reasoning by using automated theorem provers to verify (putatively) trivial proof steps.

Relevant Publications:

2018, CSEDU: MD and Krysia Broda, Intuitive Reasoning in Formalized Mathematics with Elfe

2019, ThEDU (EPTCS): MD and Krysia Broda, Towards Intuitive Reasoning in Axiomatic Geometry

Biography

I did my DPhil in Oxford under the supervision of Samson Abramsky and Sam Staton. Before coming to Oxford, I completed a master's in Logic and Philosophy of Science at the MCMP at LMU Munich. In my master's thesis, I tried to give philosophical underpinning to why a classical mathematician should embrace constructive reasoning and, conversely, why a type theorist can have peace of mind being a realist about mathematics. And before that, I did a bachelor's in Computer Science and Mathematics at RWTH Aachen. I spent the last year of my bachelor's at Imperial College London, where I worked with Krysia Broda on the Elfe prover