Jonathan Laurent

I am a PhD researcher at Carnegie Mellon University and at the Karlsruhe Institute of Technology. My current research interests lie at the intersection of machine learning and automated theorem proving. My goal is to implement an AlphaZero-like agent capable of self-learning to prove and discover mathematical theorems without human supervision.

Previously, I developed techniques to uncover the causal structure of simulation trajectories generated from rule-based models of complex biochemical systems, in collaboration with Harvard Medical School. I am also passionate about teaching and programming in Julia or OCaml.

Jonathan Laurent


Selected Publications

Learning to Find Proofs and Theorems by Learning to Refine Search Strategies:
The Case of Loop Invariant Synthesis
Jonathan Laurent, André Platzer Abstract Paper Code Poster
NeurIPS 2022
Counterfactual Resimulation for Causal Analysis of Rule-Based Models
Jonathan Laurent, Jean Yang, Walter Fontana Abstract Paper
IJCAI 2018

A complete list of publications can be found here.


I am the lead developer of AlphaZero.jl:

I am also actively developing and maintaining the following programs for the Kappa simulation platform:

  • KaTie: a domain-specific language for analyzing Kappa simulation traces.
  • Kappa Counterfactual Resimulator: a library to sample counterfactual traces in Kappa.
  • KaFlow: a program to generate causal summaries of Kappa traces.

Finally, I developed the Copilot Theorem package, which enables fully-automated verification of safety properties of real-time embedded programs written in the Copilot language.


I enjoy meeting new people and talking about research. In particular, if you are a potential collaborator or a student interested in a research project, do not hesitate to send me an email.

  • Email:,
  • Address: Karlsruhe Institute of Technology, Am Fasanengarten 5, 76131 Karlsruhe, Germany
  • Office: Building 50.34, Room 158
  • ORCID ID: 0000-0002-8477-1560