I am a distinguished researcher at the Czech Institute of of Informatics, Robotics and Cybernetics (CIIRC) heading the ERC Consolidator project AI4REASON. Before that I was a postdoc researcher in the Foundations Group of ICIS at the Radboud University, Nijmegen, an assistant professor at the Department of Theoretical Computer Science and Mathematical Logic at Charles University in Prague (I co-founded the Prague Automated Reasoning Group), and a Marie-Curie fellow at the Department of Computer Science at University of Miami. (Scientific CV)

M.S. in Mathematics (1998), Faculty of Mathematics and Physics, Charles University, Prague, (English summary)

B.S. in Economics (1995), Faculty of Social Sciences, Charles University, Prague

*
*

Here is a 2013 interview, a 2013 2-page paper (coming with a talk and slides) and a 2012 longer paper explaining what I have been doing for more than a decade and why. A lot of motivation is also in my earliest JAR paper about the first AI/ATP experiments done over Mizar in 2003. In 2014, I declared several AI/TP challenges and bets, and in 2018, I gave a long AGI 2018 keynote "No one shall drive us from the semantic AI paradise of computer-understandable math and science". Some history bits and motivation seen from 2021 are in an episode of Sean Welleck's Thesis Review Podcast. In 2023, I gave a long interview about my research and AI/TP topics to Hykel Hosni at The Reasoner.

- Machine Learner for Automated Reasoning (MaLARea) (IJCAR'08 paper, CASC'20 results, CASC'18 results, CASC'13 results, CASC'12 results)
- ENIGMA: Efficient Learning-Based Inference Guiding Machine (Papers: CICM'17 CICM'18 CADE'19 TABLEAUX 2019 ITP'19 IJCAR'20 )
- Automated Reasoning and Presentation Services for Mizar (MizAR) (JAR 2013 paper, Mizar 40 paper)
- HOL(y)Hammer: Learning-assisted Automated Reasoning for HOL Light (main paper, service description, 47% strengthening, lemmatization)
- BliStr: The Blind Strategymaker (paper, slides)
- Machine Learning Connection Prover (MaLeCoP) (the prototype is here)
- Mizar Problems for Theorem Proving (MPTP) (JAR paper on 1st version, and JAR paper on 2nd version)
- MoMM (Most of Mizar|Math Matches) (IJAIT paper)
- Mizar mode for Emacs (JAL paper)
- XML-based API to Mizar and transformations based on it (MKM paper)
- E-MaLeS (Machine Learning of Strategies for E) (CADE'12 paper)
- The Mizar-TPTP Semantic Presentation and Verification (SLGR paper)
- Mizar Proof Advisor
- Formal mathematics in a wiki (MathWiki)
- Machine learning for automated reasoning (Learning2Reason)
- Translation between Informal and Formal Mathematics (poster)
- The MPTP $100 Challenges
- Formal articles on large cardinals: Basic Facts about Inaccessible and Measurable Cardinals, Mahlo and Inaccessible Cardinals
- Formal articles on order-sorted algebras: OSALG_1, OSALG_2, OSALG_3, OSALG_4, OSAFREE,
- my GitHub (containing some more systems)
- Mizar TWiki (from Chaos all things were born :-)

- Mark Adams (PhD)
- Filip Bartek (PhD)
- Lasse Blaauwbroek (PhD)
- Zarathustra Goertzel (PhD)
- Yutaka Nagashima (PhD)
- Jelle Piepenbrock (PhD)
- Bartosz Piotrowski (PhD)
- Liao Zhang (PhD)

- Daniel Kuehlwein (PhD)
- Krystof Hoder (MSc - finished in Manchester)
- Ondrej Kuncar (MSc, PhD - finished at Munich)
- Martin Smolik (MSc)

**Contact details:**

Czech Institute of Informatics, Robotics, and Cybernetics

Czech Technical University in Prague

Zikova 4

166 36 Prague 6

Czech Republic

**e**:
josef DOT urban AT
gmail DOT com
**t**: +420-22435-4191

(partially) updated: March 8 2021