Adrian De Lon

I’m a researcher at AI4REASON in Prague and a PhD candidate in formal mathematics and logic at the Bonn International Graduate School of Mathematics, the PhD programme of the Hausdorff Center for Mathematics.

My research interest lies in bridging the gap between the informal and formal. I work on machine reasoning, informalization, and autoformalization under the supervision of Josef Urban and on Felix, a new iteration of the Naproche proof assistant, under the supervision of Peter Koepke.

Currently I'm focussed on modelling textbook mathematical proofs, using automated theorem proving to fill gaps in informal reasoning.

Mail: adelon@uni-bonn.de

Publications

The Naproche-ZF theorem prover

IJCAR 2024 (short paper)

System description of an earlier version of Felix.

Published in Springer LNCS (LNAI), volume 14739.

paper bib

The Isabelle⁠/⁠Naproche Natural Language Proof Assistant

CADE 2021

Joint work with Peter Koepke, Anton Lorenzen, Adrian Marti, Marcel Schütz, and Makarius Wenzel.

Published in Springer LNCS, volume 12699.

paper bib pdf

Beautiful formalizations in Isabelle⁠/⁠Naproche

CICM 2021

Joint work with Peter Koepke, Anton Lorenzen, Adrian Marti, Marcel Schütz, and Erik Sturzenhecker.

Published in Springer LNCS, volume 12833.

paper bib preprint

A natural formalization of the mutilated checkerboard problem in Naproche

ITP 2021

Joint work with Peter Koepke and Anton Lorenzen.

Published in LIPIcs, volume 193.

paper bib pdf

Interpreting Mathematical Texts in Naproche-SAD

CICM 2020

Joint work with Peter Koepke and Anton Lorenzen.

Published in Springer LNCS, volume 12236.

paper bib

From LaTeX to Lean with a Controlled Natural Language

CICM 2020 (informal paper)

Joint work with Peter Koepke and Anton Lorenzen.

Software

Felix

Experimental natural language proof assistant based on higher-order set theory with first-order proof automation.

source code

Naproche

A proof assistant oriented towards natural language and proof automation, distributed as part of Isabelle.

project page download source code

Talks

Towards autoformalization of textbook mathematics with natural proof checking

Invited talk at the Malinca conference Bridging the linguistic gap between the mathematician and the machine, Institut Henri Poincaré, Paris, 8–19 September 2025.

Natural language understanding in natural proof checking

Invited talk at the EuroProofNet Symposium, Institut Pascal, Orsay, 1–3 October 2025.

Le Miz s’approche: informalization and autoformalization with Mizar and Naproche

AITP 2025

Joint work with Josef Urban, Peter Koepke, Atle Hahn and Mario Carneiro.

Scaling a natural proof assistant step by step

Talk at the Workshop on Natural Formal Mathematics, Joint WG4-WG5 meeting, Cambridge, UK, 6–8 September 2023.

Scaling Naproche

AITP 2022

ForTheL for type theory

AITP 2020

Joint work with Peter Koepke and Anton Lorenzen.