AGI-26 keynote
Josef Urban
Josef Urban is a distinguished researcher at the Czech Institute of Informatics, Robotics and Cybernetics in Prague, where he heads the ERC project AI4REASON and co-founded the Prague Automated Reasoning Group.
“Automated deductive reasoning (automated theorem proving), inductive reasoning (machine learning and discovery) and their combining.”
— Josef Urban, describing his research interests, CIIRC profile
One bottleneck, moved seven times
Read the archive in order and it is the same engineering question, asked of a steadily larger part of the problem: which of the thousands of things we already know does this proof need? Each answer makes the next bottleneck visible.
-
Translation
Prague, from 2003The Mizar Mathematical Library is one of the largest bodies of machine-checked mathematics ever written, and for decades it could only be read by Mizar. Urban’s first system, MPTP, translates it into the first-order format that ordinary automated theorem provers speak — turning a library into a problem set.
MPTP 0.2: Design, Implementation, and Initial Experiments (2006) ↗ -
Selection
from 2007Translation exposes the real bottleneck. Given thousands of available facts, which handful should the prover be given? MaLARea — "a Machine Learner for Automated Reasoning" — loops a deductive prover against a learner that predicts useful premises from previous proofs, each feeding the other.
MaLARea: a Metasystem for Automated Reasoning in Large Theories (2007) ↗ -
Hammers
with Cezary KaliszykThe same machinery pointed at working mathematicians. A "hammer" takes a goal inside a proof assistant, picks relevant facts, ships them to external provers, and reconstructs what comes back. HOL(y)Hammer put one online as a service for HOL Light; the Flyspeck work measured it against a real, large formalization.
HOL(y)Hammer: Online ATP Service for HOL Light (2014) ↗ -
Learning to guide
2016–2018Then the learner moves inside the prover. DeepMath — with Alemi, Chollet, Eén, Irving and Szegedy — learns premise selection with neural sequence models, “avoiding the hand-engineered features of existing state-of-the-art models”, and claims in its own abstract to be “the first time deep learning has been applied to theorem proving on a large scale.” ENIGMA then moves the learner inside the prover’s own clause-selection loop.
DeepMath — Deep Sequence Models for Premise Selection (2016) ↗ -
Search as a game
2018–2020If proof search is a sequence of choices, it can be learned the way games are. This work runs Monte-Carlo simulations "guided by reinforcement learning from previous proof attempts", with, in its own words, "practically no domain heuristics"; TacticToe does the tactic-level counterpart inside HOL4.
Reinforcement Learning of Theorem Proving (2018) ↗ -
Conjecturing
2025The last thing a prover is given is the thing to prove. Working from 16,197 OEIS-derived problems that need both induction and arithmetic, this paper builds a feedback loop that invents the induction predicates itself, reporting 5,565 problems solved against 2,265 for CVC5, Vampire or Z3 given 60 seconds. Its title is the claim: learning conjecturing from scratch.
Learning Conjecturing from Scratch (2025) ↗ -
Autoformalization
2026And the direction reverses. Rather than translating formal libraries out to provers, this project translates an ordinary textbook in — Munkres’ general topology, 241 pages. The paper reports 160k lines of formalized topology, about 130k of them produced in two weeks, and asks in its title whether this is now cheap enough for everyone.
130k Lines of Formal Topology in Two Weeks (2026) ↗
At a conference called AGI-26
This archive is unusual on the roster in that its subject matter is checkable. A proof either goes through or it does not, and the machine that checks it does not care who wrote it. Urban’s field has spent two decades building learning systems whose output is verified by construction.
His 2024 survey with six co-authors states the opportunity plainly: automated provers are “in theory capable of proving arbitrarily hard theorems” but “in practice… face large combinatorial explosion, and therefore include many heuristics and choice points that considerably influence their performance.” Those choice points are where the learning goes.
We surface this because it is a live counter-current to how capability is usually argued about at a conference like this one — not scale alone, but search plus verification.
Read the survey ↗A field, not a solo record
Most of this archive is co-authored, and the same names recur across decades — Cezary Kaliszyk above all, then Jan Jakubův, Jiří Vyskočil, Chad E. Brown, Miroslav Olšák, Thibault Gauthier. The systems named here are group artifacts with long lives: MPTP, MaLARea, HOL(y)Hammer, ENIGMA and TacticToe all appear across multiple papers and multiple versions.
Selected work
15 entries drawn from the archive, titled exactly as the records read, with his position in the author list computed from each record. Everything else is in the corpus.
- 2026130k Lines of Formal Topology in Two Weeks: Simple and Cheap Autoformalization for Everyone? (Short Paper)Dagstuhl Research Online Publication Server sole author
- 2025Learning Conjecturing from ScratchLecture notes in computer science last of 2 authors
- 2025Hammering Higher Order Set TheoryLecture notes in computer science last of 4 authors
- 2024Learning Guided Automated Reasoning: A Brief SurveyLecture notes in computer science last of 7 authors
- 2020TacticToe: Learning to Prove with TacticsJournal of Automated Reasoning author 3 of 5
- 2018Reinforcement Learning of Theorem ProvingarXiv (Cornell University) author 2 of 4
- 2017ENIGMA: Efficient Learning-Based Inference Guiding MachineLecture notes in computer science last of 2 authors
- 2016DeepMath - Deep Sequence Models for Premise SelectionNeural Information Processing Systems last of 5 authors
- 2015Mizar: State-of-the-art and BeyondLecture notes in computer science last of 8 authors
- 2014HOL(y)Hammer: Online ATP Service for HOL LightMathematics in Computer Science last of 2 authors
- 2014Learning-Assisted Automated Reasoning with FlyspeckJournal of Automated Reasoning last of 2 authors
- 2013Premise Selection for Mathematics by Corpus Analysis and Kernel MethodsJournal of Automated Reasoning last of 5 authors
- 2007
- 2006MPTP 0.2: Design, Implementation, and Initial ExperimentsJournal of Automated Reasoning sole author
- 2003Translating Mizar for First Order Theorem ProversLecture notes in computer science sole author
Background
- Now
- Distinguished researcher, Czech Institute of Informatics, Robotics and Cybernetics (CIIRC), Prague. Heads the ERC Consolidator project AI4REASON; co-founder of the Prague Automated Reasoning Group.
- Education
- Ph.D. Computer Science (2004), Faculty of Mathematics and Physics, Charles University, Prague · M.S. Mathematics (1998), same faculty · B.S. Economics (1995), Faculty of Social Sciences, Charles University.
- Systems
- MPTP (Mizar Problems for Theorem Proving), MaLARea, HOL(y)Hammer with Cezary Kaliszyk, ENIGMA, and TacticToe — each appearing in this corpus across several papers and versions.
About this archive
This is an independent archive of Josef Urban’s publication record, built for Society of Minds Aligned and AGI-26. Records span 2003–2026 and are drawn from OpenAlex; preprints and versions of record are both kept, so the archive is a reading index, not a bibliometric count.
“Josef Urban” is a common Czech name, and the harvest returned at least four different people who share it. Twenty-one records — in genetics, polymer chemistry, telecommunications and elsewhere — were removed by hand and are listed, with the reason, in the archive’s exclusion manifest. Biography, degrees and the quotation above come from his CIIRC profile.
Not written by, reviewed by, or endorsed by Josef Urban. If you are Josef and something here is wrong, the feedback control at the bottom of the page reaches us directly — and the claim bar will hand you the site.