Alexander Bentkamp
I am a postdoctoral researcher at the LMU Munich. My main research interests are interactive and automated theorem proving. I have a PhD in computer science from the Vrije Universiteit Amsterdam.
I am a postdoctoral researcher at the LMU Munich. My main research interests are interactive and automated theorem proving. I have a PhD in computer science from the Vrije Universiteit Amsterdam.
We reimplemented the Natural Number Game in Lean 4 with a brand-new user interface concept
Play now!My thesis won the Ackermann Award, the Beth Award, the McCune Award, and the IPA dissertation award!
Thesis (PDF)The article "Mechanical Mathematicians" has been accepted by the Communications of the ACM.
Preprint (PDF)
Complete and efficient higher-order reasoning via lambda-superposition
Alexander Bentkamp, Jasmin Blanchette, Visa Nummelin, Sophie Tourret, and Uwe Waldmann.
Draft (PDF)
Finding mathematical proofs using computers
Alexander Bentkamp, Jasmin Blanchette.
Nieuw Archief voor Wiskunde 5/24(2): 114–118, 2023
Publisher's PDF ⋅
Preprint (PDF)
Verified Reductions for Optimization
Alexander Bentkamp, Ramon Fernández Mir, Jeremy Avigad.
In: Sankaranarayanan, S., Sharygina, N. (eds.) Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2023), LNCS, Springer.
Publisher's page ⋅
Preprint (PDF)
HHLPy: Practical Verification of Hybrid Systems using Hoare Logic
Huanhuan Sheng, Alexander Bentkamp, Bohua Zhan.
In: Chechik, M., Katoen, JP., Leucker, M. (eds.) Formal Methods (FM 2023),
LNCS, Springer.
Publisher's page ⋅
Preprint (PDF)
Superposition for Higher-Order Logic
Alexander Bentkamp, Jasmin Blanchette, Sophie Tourret, and Petar Vukmirović.
Journal of Automated Reasoning 67: Article number: 10, 2023.
Publisher's page ⋅
Preprint (PDF) ⋅
Errata (PDF)
Privacy accounting εconomics: Improving differential privacy composition via a posteriori bounds
Valentin Hartmann, Vincent Bindschaedler, Alexander Bentkamp, Robert West.
Proceedings on Privacy Enhancing Technologies 2022(3): 222–246, 2022.
Publisher's page ⋅
Preprint (PDF)
An Impossible Asylum
Jeremy Avigad, Seulkee Baek, Alexander Bentkamp, Marijn Heule, and Wojciech Nawrocki.
The American Mathematical Monthly, 130:5, 446-453
Publisher's page ⋅
Preprint (PDF)
Mechanical Mathematicians
Alexander Bentkamp, Jasmin Blanchette, Visa Nummelin, Sophie Tourret, Petar Vukmirović, and Uwe Waldmann.
Communications of the ACM 66(4): 80–90, 2023
Preprint (PDF)
Verified Optimization (work in progress)
Alexander Bentkamp and Jeremy Avigad.
In Blanchette, J., Naumowicz, A. (eds.) Fifth Workshop on Formal Mathematics for Mathematicians (FMM 2021),
CEUR Workshop Proceedings (CEUR-WS.org).
Preprint (PDF)
Efficient full higher-order unification
Petar Vukmirović, Alexander Bentkamp, and Visa Nummelin.
Logical Methods in Computer Science 17(4): 18:1–18:31, 2021.
Publisher's page ⋅
Authors' PDF
The Embedding Path Order for Lambda-Free Higher-Order Terms
Alexander Bentkamp.
Journal of Applied Logics 8(10): 2447-2469, 2021.
Publisher's page ⋅
Authors' PDF ⋅
Supplementary material ⋅
Slides (PDF)
Superposition for full higher-order logic
Alexander Bentkamp, Jasmin Blanchette, Sophie Tourret, and Petar Vukmirović.
In Platzer, A., Sutcliffe, G. (eds.) 28th International Conference on Automated Deduction (CADE-28),
LNCS, Springer, 2021.
Publisher's page ⋅
Authors' PDF ⋅
Report (PDF) ⋅
Slides (PDF) ⋅
Errata (PDF)
Superposition with first-class Booleans and inprocessing clausification
Visa Nummelin, Alexander Bentkamp, Sophie Tourret, and Petar Vukmirović.
In Platzer, A., Sutcliffe, G. (eds.) 28th International Conference on Automated Deduction (CADE-28),
LNCS, Springer, 2021.
Publisher's page ⋅
Authors' PDF ⋅
Report (PDF) ⋅
Errata (PDF)
Making Higher-Order Superposition Work
Petar Vukmirović, Alexander Bentkamp, Jasmin Blanchette, Simon Cruanes, Visa Nummelin, and Sophie Tourret.
In Platzer, A., Sutcliffe, G. (eds.) 28th International Conference on Automated Deduction (CADE-28),
LNCS, Springer, 2021.
Publisher's page ⋅
Authors' PDF
Superposition with lambdas
Alexander Bentkamp, Jasmin Blanchette, Sophie Tourret, Petar Vukmirović, and Uwe Waldmann.
Journal of Automated Reasoning 65: 893–940, 2021.
Publisher's page ⋅
Authors' PDF ⋅
Supplementary material
Superposition for lambda-free higher-order logic
Alexander Bentkamp, Jasmin Blanchette, Simon Cruanes, and Uwe Waldmann.
Logical Methods in Computer Science 17(2): 1:1–1:38, 2021.
Publisher's page ⋅
Authors' PDF ⋅
Supplementary material
Efficient full higher-order unification
Petar Vukmirović, Alexander Bentkamp, and Visa Nummelin.
In Ariola, Z.M. (ed.), 5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020),
LIPIcs 167, pp. 5:1–5:17, Schloss Dagstuhl—Leibniz-Zentrum für Informatik, 2020.
Publisher's page ⋅
Authors' PDF ⋅
Report (PDF)
Superposition with lambdas
Alexander Bentkamp, Jasmin Christian Blanchette, Sophie Tourret, Petar Vukmirović, and Uwe Waldmann.
In Fontaine, P. (ed.) 27th International Conference on Automated Deduction (CADE-27),
LNCS 11716, pp. 55–73, Springer, 2019.
Publisher's page ⋅
Authors' PDF ⋅
Report (PDF) ⋅
Slides (PDF)
A formal proof of the expressiveness of deep learning
Alexander Bentkamp, Jasmin Christian Blanchette, and Dietrich Klakow. Journal of Automated Reasoning 63(2), pp. 347-368, 2019.
Publisher's page ⋅
Authors' PDF
Superposition for lambda-free higher-order logic
Alexander Bentkamp, Jasmin Christian Blanchette, Simon Cruanes, and Uwe Waldmann.
In Galmiche, D., Schulz, S., Sebastiani, R. (eds.) 9th International Joint Conference on Automated Reasoning (IJCAR 2018),
LNCS 10900, pp. 28–46, Springer, 2018.
Publisher's page ⋅
Authors' PDF ⋅
Report (PDF) ⋅
Slides (PDF) ⋅
Supplementary material
A formal proof of the expressiveness of deep learning
Alexander Bentkamp, Jasmin Christian Blanchette, and Dietrich Klakow.
In Ayala-Rincón, M., Muños, C. A. (eds.) 8th Conference on Interactive Theorem Proving (ITP 2017),
LNCS 10499, pp. 46–64, Springer, 2017.
Web page ⋅
Authors' PDF ⋅
Slides (PDF)
An Isabelle formalization of the expressiveness of deep learning (extended abstract)
Alexander Bentkamp, Jasmin Christian Blanchette, and Dietrich Klakow. In Hales, T. C., Kaliszyk, C., Schulz, S., Urban, J. (eds.) 2nd Conference on Artificial Intelligence and Theorem Proving (AITP 2017), pp. 22–23.
Abstract (PDF) ⋅
Slides (PDF)
Superposition for Higher-Order Logic
Alexander Bentkamp. Ph.D. thesis, Vrije Universiteit Amsterdam, 2021.
PhD Thesis (PDF) ⋅
Errata (PDF)
An Isabelle formalization of the expressiveness of deep learning
Alexander Bentkamp. M.Sc. thesis, Universität des Saarlandes, 2016.
MSc Thesis (PDF)
Homologische Betrachtung des Alexanderpolynoms
Alexander Bentkamp. B.Sc. thesis, Georg-August-Universität Göttingen, 2013.
BSc Thesis (PDF)