Curriculum vitae
Address at the Mathematical Institute
| Name | Adrian De Lon |
| Address | Endenicher Allee 60, D‑53115 Bonn |
| Room | N2.003 (in the annexe) |
Education and affiliations
| 2023 | CIIRC CTU Prague Research stay (6 months) |
| 2021–now | University of Bonn Bonn International Graduate School of Mathematics PhD programme in Mathematics (Formal Mathematics and Logic) |
| 2018–2020 | University of Bonn M Sc Mathematics |
| 2015–2018 | Johannes Gutenberg University of Mainz B Sc Mathematics (with a minor in Theoretical Physics) |
Publications and conference contributions
| IJCAR 2024 | The Naproche-ZF theorem prover (short paper/system description) International Joint Conference on Automated Reasoning, Nancy, France, 1–6 July 2024 (to appear) |
| NatFoM ’23 | Scaling a natural proof assistant step by step (talk) Workshop on Natural Formal Mathematics at the Joint WG4-WG5 meeting, Cambridge, UK, 6–8 September 2023 (slides available) |
| AITP 2022 | Scaling Naproche (talk) |
| CADE 2021 | The 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 (open access, CC BY 4.0 license, PDF available) |
| CICM 2021 | Beautiful Formalizations in Isabelle/Naproche with Peter Koepke, Anton Lorenzen, Adrian Marti, Marcel Schütz, and Erik Sturzenhecker in Springer Lecture Notes in Computer Science, volume 12833 (closed access, preprint PDF available) |
| ITP 2021 | A Natural Formalization of the Mutilated Checkerboard Problem in Naproche with Peter Koepke and Anton Lorenzen in Leibniz International Proceedings in Informatics, volume 193 (open access, CC BY 4.0 license, PDF available) |
| CICM 2020 | Interpreting Mathematical Texts in Naproche-SAD (proceedings) with Peter Koepke and Anton Lorenzen in Springer Lecture Notes in Computer Science, volume 12236 |
| CICM 2020 | From LaTeX to Lean with a Controlled Natural Language (informal paper) with Peter Koepke and Anton Lorenzen |
| AITP 2020 | ForTheL for Type Theory (talk) with Peter Koepke and Anton Lorenzen |
Service and organizational work
| 2024–now | Vice leader of work group 5 (machine learning) of the European Cooperation in Science and Technology action CA20111 (EuroProofNet) and member of the EuroProofNet Core Group |
Teaching and tutoring work
| Summer 2024 | Practicum Mathematical Logic (together with Peter Koepke) |
| Winter 2023/24 | Hauptseminar Applied Mathematical Logic (together with Peter Koepke) |
| Winter 2023/24 | Practicum Mathematical Logic (together with Peter Koepke) |
| Winter 2022/23 | Teaching assistant for Automated Proving (with Peter Koepke) |
| November 2022 | Assistant for Plücker Lectures (Lean sessions) |
| Summer 2022 | Teaching assistant for Foundations and Implementations of Automated and Interactive Theorem Proving (with Peter Koepke) |
| Winter 2021/22 | Teaching assistant for Model Theory (with Philipp Hieronymi) |
| Summer 2021 | Teaching assistant for Logic (with Philipp Schlicht) |
| Summer 2020 | Tutor for Geometry and Topology (with Markus Hausmann) |
| Winter 2019/20 | Tutor for Logic (with Peter Koepke) |
| Summer 2019 | Tutor for Geometry and Topology (with Ursula Hamenstädt) |
| Winter 2018/19 | Tutor for Linear Algebra (with Daniel Huybrechts) |
| Winter 2017/18 | Tutor for Mathematics for Physics (with Matthias Schneider) |
| Summer 2017 | Tutor for Linear Algebra and Geometry (with Felix Leinen) |
| Summer 2017 | Course on LaTeX (on request from the student association) |