My research interests include formalization of mathematics and the use of computational methods in formalization, type theory, category theory.
Projects
-
FormalTT
A formalization of simple type theory in Agda
-
Lean-HoG
A library for computational graph theory in Lean 4, with emphasis on verification of large datasets of graphs; in particular the House of Graphs (HoG).
Papers
- Incorporating a Database of Graphs into a Proof Assistant In: Kohlhase, A., Kovács, L. (eds) Intelligent Computer Mathematics. CICM 2024. Lecture Notes in Computer Science, vol 14960. Springer, Cham.