Adrian De Lon
Researcher
CIIRC CTU Prague

About me

I’m a reseracher at CIIRC 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.

I work on machine reasoning, informalization, and autoformalization under the supervision of Josef Urban and on Naproche-ZF, a new iteration of the Naproche proof assistant under the supervision of Peter Koepke. My research interest lies in bringing formal mathematics closer to informal mathematics.

Selected publications

IJCAR 2024The Naproche-ZF theorem prover (short paper/system description)
in Automated Reasoning (IJCAR 2024), Springer LNAI,volume 14739
CADE 2021The Isabelle/Naproche Natural Language Proof Assistant (system description)
with Peter Koepke, Anton Lorenzen, Adrian Marti, Marcel Schütz, and Makarius Wenzel
in Springer Lecture Notes in Computer Science, volume 12699
PDF download (0.45 MB)
ITP 2021A Natural Formalization of the Mutilated Checkerboard Problem in Naproche
with Peter Koepke and Anton Lorenzen
in Leibniz International Proceedings in Informatics, volume 193
PDF download (0.35 MB)

The full list of my publications and conference contributions can be found on my cv.

Software projects

NaprocheA proof assistant oriented towards natural language and proof automation. Naproche is distributed as a part of Isabelle.
Naproche‑ZFExperimental natural language proof assistant based on higher-order set theory with first-order proof automation.