Jonathan Laurent

I am a PhD candidate at Carnegie Mellon University and a former student of the École Normale Supérieure (Paris). 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.

Email address:
Jonathan Laurent


I will be giving a talk at JuliaCon 2021: “Building on AlphaZero with Julia”.

July 2021

I will be giving a talk at AITP 2021 about my research on applying reinforcement learning to proof search and program synthesis: “Designing a Theorem Prover for Reinforcement Learning and Neural Guidance”.

July 2021

Julia Computing demoed AlphaZero.jl during their JuliaCon 2020 sponsor talk.

August 2020

I am releasing AlphaZero.jl, an implementation of Deepmind’s algorithm in Julia. It is one to two orders of magnitude faster than existing Python implementations, while being equally simple.

April 2020

Featured 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
NeurIPS 2022
Counterfactual Resimulation for Causal Analysis of Rule-Based Models
Jonathan Laurent, Jean Yang, Walter Fontana Abstract Paper
IJCAI 2018
A Trace Query Language for Kappa
Jonathan Laurent, Hector Medina Abarca, Pierre Boutillier, Jean Yang, Walter Fontana Abstract Paper
CMSB 2018

A complete list of publications can be found here.


I am the lead developer of AlphaZero.jl.

  • The philosophy of this project is to provide an implementation of AlphaZero that is simple enough to be widely accessible for students and researchers, while also being sufficiently powerful and fast to enable meaningful experiments on limited computing resources.
  • AlphaZero.jl is consistently one to two orders of magnitude faster than existing Python implementations, while being equally simple and flexible.

I am also actively developing and maintaining the following programs:

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.