Josef Urban

Timeline

1. 1995–2004

   Three degrees at Charles University

   He earns a B.S. in economics at Charles University's Faculty of Social Sciences in 1995 and an M.S. in mathematics at its Faculty of Mathematics and Physics in 1998. He completes a computer science Ph.D. at the Faculty of Mathematics and Physics in 2004.

2. 2003–2013

   Opening Mizar to AI

   In 2003, he makes the Mizar library of formal mathematics available to automated theorem proving and AI methods, and co-founds the Prague Automated Reasoning Group. By 2013, his MaLARea system combines proof deduction with machine-learning guidance and solves most problems in CASC's Large Theory division.

3. 2006–2013

   Posts in Miami, Prague and Nijmegen

   From 2006 to 2008, he is a Marie-Curie fellow in the University of Miami's Department of Computer Science. By 2013, he is a postdoctoral researcher in the Foundations Group of ICIS at Radboud University Nijmegen, after an assistant professorship in Charles University's Department of Theoretical Computer Science and Mathematical Logic.

4. October 2016

   Leading AI4REASON at CIIRC

   By October 2016, he is a principal researcher at the Czech Institute of Informatics, Robotics and Cybernetics and leads the ERC Consolidator project AI4REASON.

5. 2018

   Reinforcement learning for theorem proving

   In 2018, he coauthors Reinforcement Learning of Theorem Proving with Cezary Kaliszyk, Henryk Michalewski and Mirek Olšák. Its prover uses reinforcement learning from earlier attempts to guide connection-style proof search and solves over 40% more problems than a baseline under the same number of inferences.

6. 2025

   Learning conjectures from scratch

   In 2025, he coauthors Learning Conjecturing from Scratch with Thibault Gauthier. Their self-learning method generates induction predicates for 16,197 problems derived from the OEIS and solves 5,565, compared with 2,265 solved by CVC5, Vampire or Z3 in 60 seconds.

7. 2026

   130k lines of formal topology

   In 2026, he submits a paper describing a feedback loop between a large language model and a proof checker that autoformalizes about 130,000 lines of topology, with most lines produced over two weeks across December 2025 and January 2026.

8. Since 2026

   Researcher at Chalmers

   In January 2026, he joins Chalmers as a researcher in Data Science and AI. In October 2026, he leads NextReason, an ERC-funded project on theorem proving, conjecture generation, neuro-symbolic reasoning and learning-based methods for mathematical reasoning.