Thomas Ammer

Contact

[email protected]

[email protected]

Bio

Since October 2023, I am a PhD student under supervision of Mohammad Abdulaziz at King's College London.
Before that, I did my Bachelor's (completion in September 2021) and Master's degree (completion in October 2023) at the
Technical University of Munich (TUM).

My interests are the formalisation of algorithms for combinatorial optimisation problems in Isabelle.

Publications

• A Formal Analysis of Algorithms for Matroids and Greedoids
  together with Mohammad Abdulaziz, Shriya Meenakshisundaram and Adem Rimpapa
  published in proceedings of the 16th International Conference on Interactive Theorem Proving (ITP), 2025
• Formal Analysis of Capacity Scaling Algorithms for Minimum Cost Flows
  together with Mohammad Abdulaziz
  published in proceedings of the 15th International Conference on Interactive Theorem Proving (ITP), 2024

• Formalisation of Combinatorial Optimisation in Isabelle/HOL: Network Flows
  Cambridge Seminar Series on Formalisation of mathematics with interactive theorem provers, February 2025, University of Cambridge [Slides]
• Formalising and Verifying Algorithms for the Minimum Cost Flow Problem
  Trimester Program Prospects for Formal Mathematics hosted at Hausdorff Research Institute for Mathematics, June 2024, Bonn, Germany [Slides]

• A Formal Analysis of Algorithms for Matroids and Greedoids, talk in Software Systems Group at the Department of Informatics at KCL,
  extended version of conference talk (see next item), December 25 [Slides]
• A Formal Analysis of Algorithms for Matroids and Greedoids, conference talk at ITP 25 (see paper above), Reykjavik, Iceland [Slides]
• Formalising Combinatorial Optimisation in Isabelle/HOL, lightning talk at VeTSS Summer School, August 25, Glasgow [Slides]
• An Isabelle/HOL Formalisation of Scaling Algorithms for Minimum Cost Flows, conference talk at ITP 24 (see paper above), Tbilisi, Georgia [Slides]

Flows (theory for maxflow and mincost flow, scaling, Orlin's Algorithm, Dinic's Algorithm), Matroid Intersection
and a few other things in the Isabelle Graph Library

Two formalisations published in the Archive of Formal Proofs:

• van Emde Boas Trees (2021)
• Number Theoretic Transform (2022)

Funding, Grants, Memberships

• LMS Travel Grant for Early Career Researchers to attend ITP 2025
• For the PhD, I am receiving an NMES Faculty Studentship from King's
• best.in.tum membership, special programme for the top 2% at TUM's Department of Informatics
• Stipendiat der Bischöflichen Studienförderung des Cusanuswerks during Bachelor's and Master's