Maximilian Doré
Maximilian Doré
Room
415,
Wolfson Building,
Parks Road, Oxford OX1 3QD
United Kingdom
Themes:
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.