Johannes Hölzl

I'm currently at CMU's Department of Philosophy with Jeremy Avigad. Working with the Lean Theorem Prover.

I studied computer science, with mathematics as minor subject, at the TU München since 2004. From May 2009 until October 2012 I was a graduate student as part of the PUMA graduate school. From 2013 until January 2017 I was working on the DFG project Ni/491 15-1. Since February 2017 I'm at CMU.

My interest is mostly formalizing mathematics in interactive theorem provers. I'm currently working on basic automation and library for Lean. I worked in Isabelle's higher-order logic, worked on its analysis, developed its measure and probability theory, and used this to verify probabilistic software.

Wir müssen wissen,
wir werden wissen. - David Hilbert


Journal Articles

Conference Proceedings



Diploma thesis

Current Work

Verification of probabilistic models in the interactive theorem prover Isabelle/HOL
I'm working on the DFG project Ni 491/15-1 and Ni 491/16-1.

Past Work

Measure, Probability, and Information
Together with Armin Heller I formalized the first three chapters of Heinz Bauer's textbook about measure theory. This is now officially part of the Isabelle repository. We built on the work from Aaron Coble which was ported to Isabelle by Lawrence C. Paulson. This work is now largely rewritten and extended, for an overview see my thesis and the work on the Giry monad, on Markov models, on the central limit theorem (CTL), and on Markov processes.
Multivariate Analysis
Robert Himmelmann ported large parts of the formalization of Multivariate Analysis available in HOL Light. The current development is found in the Isabelle repository.
Up Down
I'm working together with Dirk Pflüger on the publication of the verification of the up-down algorithm.
Verification of Sparse Matrix codes
Gilad Arnold and I are working on automatically verifying the correctness of Sparse Matrix codes.
Diploma thesis
Proving Real-Valued Inequalities by Computation in Isabelle/HOL
Developing Isabelle user interface components for interactive Prover-IDEs based on jEdit. This is the origin of isabelle-jedit.
Verifying the up-down algorithm