Urban

CV

Scientific CV of Josef Urban, Ph.D.
CIIRC, Czech Technical University in Prague,
Josef.Urban@gmail.com, ciirc.cvut.cz/~urbanjo3/
Jugoslavskych partyzanu 1580/3, 16000 Praha 6 – Dejvice, Czech Republic
Phone: +420224354191
Education: Charles University in Prague, Czech Republic
10/98 - 12/04
10/92 - 9/98
10/92 - 6/95

Ph.D. in Computer Science
M.S. in Mathematics
B.S. in Economics

Position:
9/15 - ongoing
9/09 - 8/15
3/09 - 6/09
4/06 - 10/07
7/05 - 3/09
2/04 - 8/04, 2/02 - 8/02

Faculty of Mathematics and Physics
Faculty of Mathematics and Physics
Faculty of Social Sciences

Distinguished Researcher, CIIRC, CTU
Postdoc researcher, Intelligent Systems, Radboud University Nijmegen
Visiting researcher, College of Engineering, American University in Armenia
Visiting Marie Curie researcher, University of Miami, Dept. of Comp. Sci.
Assistant professor, Dept. of Theoretical Comp. Science, Charles University
Young Visiting Researcher, Dept. of Comp. Science, University of Bialystok

Research Interests:
Automated Reasoning, Artificial Intelligence, Formal Mathematics and Verification, Machine Learning,
Semantic KBs, Automated Reasoning in Large Theories, Combining Deductive and Inductive Reasoning
Selected Funding:2021 - 2022
Combining Neural and Symbolic Methods in Theorem Proving, Amazon ResearchAwards 2021 - AWS Automated Reasoning, PI, USD 60000
6/17 - ongoing Artificial Intelligence and Reasoning, Excellent Research Teams - Czech Ministry of
Education and EU Regional Development Fund, PI, CZK 127311541 (∼ EUR 5M)
9/15 - 10/20
AI for Large-Scale Computer-Assisted Reasoning, ERC Consolidator, PI, EUR 1.5M
2017
Google Faculty Research Award 2016, PI, USD 35000
9/12 - 8/15
Knowledge-based Automated Reasoning, NWO, PI and postdoc, EUR 205000
9/10 - 8/15
Learning to Reason: a Machine Learning Approach for Computer-Assisted Reasoning, NWO PhD funding, Co-investigator, EUR 205000
9/09 - 8/12
MathWiki a Web-based Collaborative Authoring Environment for Formal Proofs,
NWO, Postdoc researcher, EUR 362406
4/06 - 6/08
Automated Reasoning in Large Formal Mathematical Knowledge Bases, Marie-Curie
Fellowship, (MOIF-CT-2005-21875), Principal investigator, EUR 176076.5
4/05 - 12/06
Tools and Formats for Automated Theorem Proving in Large Mathematical Knowledge Bases, Charles University grant (205-10/203336), Co-investigator, CZK 553000
2/04 - 8/04,
CALCULEMUS, European Marie-Curie Research Training Network –2/02 - 8/02
– (HPRN-CT-2000-00102), Young Visiting Researcher
Publications and Citations as of November 2021:
128 published/accepted papers (34 journal, 3 book chapters, 91 papers in proceedings), 13 edited volumes.
Citations by Google Scholar (total/since 2016): 4511/3137 citations, 37/28 h-index, 90/70 i10-index.
Google Scholar profile: https://scholar.google.com/citations?user=4pW-Je4AAAAJ .
DBLP profile: https://dblp.org/pers/hd/u/Urban:Josef .
Journal Articles:

1.

Gauthier, T., Kaliszyk, C., Urban, J., Kumar, R. & Norrish, M. TacticToe: Learning to Prove with
Tactics. J. Autom. Reason. 65, 257–286 (2021).

Page 1 of 14

Urban
2.
3.
4.
5.
6.
7.
8.
9.
10.
11.

12.
13.
14.
15.
16.
17.
18.
19.
20.
21.
22.
23.
24.
25.
26.

CV
Färber, M., Kaliszyk, C. & Urban, J. Machine Learning Guidance for Connection Tableaux. J.
Autom. Reason. 65, 287–320 (2021).
Labahn, G., Davenport, J. & Urban, J. Foreword (to special issue on ICMS 2018). English. Mathematics in Computer Science (2020).
Jakubuv, J. & Urban, J. Hierarchical invention of theorem proving strategies. AI Commun. 31,
237–250 (2018).
Fontaine, P., Kaliszyk, C., Schulz, S. & Urban, J. Foreword to the Special Issue on AutomatedReasoning. AI Commun. 31, 235–236 (2018).
Hales, T. et al. A Formal Proof of the Kepler Conjecture. Forum of Mathematics, Pi 5, e2 (2017).
Blanchette, J. C., Kaliszyk, C., Paulson, L. C. & Urban, J. Hammering towards QED. J. Formalized
Reasoning 9, 101–148 (2016).
Sutcliffe, G. & Urban, J. The CADE-25 Automated Theorem Proving system competition - CASC25. AI Commun. 29, 423–433 (2016).
Blanchette, J. C., Greenaway, D., Kaliszyk, C., Kühlwein, D. & Urban, J. A Learning-Based Fact
Selector for Isabelle/HOL. J. Autom. Reasoning 57, 219–244 (2016).
Harrison, J., Urban, J. & Wiedijk, F. Preface: Twenty Years of the QED Manifesto. J. Formalized
Reasoning 9, 1–2 (2016).
Wiedijk, F., Geuvers, H. & Urban, J. Een wiskundig bewijs correct bewezen: De meest efficiente
manier om bollen op te stapelen (in Dutch). Nieuw Archief voor Wiskunde (NAW) 5/17, 177–183(2016).
Kühlwein, D. & Urban, J. MaLeS: A Framework for Automatic Tuning of Automated Theorem
Provers. J. Autom. Reasoning 55, 91–116 (2015).
Kaliszyk, C. & Urban, J. MizAR 40 for Mizar 40. J. Autom. Reasoning 55, 245–256 (2015).
Kaliszyk, C. & Urban, J. Learning-assisted theorem proving with millions of lemmas. J. Symb.
Comput. 69, 109–128 (2015).
Kaliszyk, C. & Urban, J. HOL(y)Hammer: Online ATP Service for HOL Light. Mathematics in
Computer Science 9, 5–22 (2015).
Alama, J., Heskes, T., Kühlwein, D., Tsivtsivadze, E. & Urban, J. Premise Selection for Mathematics
by Corpus Analysis and Kernel Methods. J. Autom. Reasoning 52, 191–213 (2014).
Kaliszyk, C. & Urban, J. Learning-Assisted Automated Reasoning with Flyspeck. J. Autom. Reasoning 53, 173–213 (2014).
Iancu, M., Kohlhase, M., Rabe, F. & Urban, J. The Mizar Mathematical Library in OMDoc: Translation and Applications. J. Autom. Reasoning 50, 191–202 (2013).
Urban, J., Rudnicki, P. & Sutcliffe, G. ATP and Presentation Service for Mizar Formalizations. J.
Autom. Reasoning 50, 229–241 (2013).
Urban, J., Sutcliffe, G., Trac, S. & Puzis, Y. Combining Mizar and TPTP Semantic Presentation
and Verification Tools. Studies in Logic, Grammar and Rhetoric 18, 121–136 (2009).
Urban, J. & Sutcliffe, G. ATP-based Cross-Verification of Mizar Proofs: Method, Systems, and First
Experiments. Mathematics in Computer Science 2, 231–251 (2008).
Urban, J. & Bancerek, G. Presenting and Explaining Mizar. Electron. Notes Theor. Comput. Sci.
174, 63–74 (2007).
Urban, J. Momm - Fast Interreduction and Retrieval in Large Libraries of Formalized Mathematics.
Int. J. Artif. Intell. Tools 15, 109–130 (2006).
Urban, J. MizarMode - an integrated proof assistance tool for the Mizar way of formalizing mathematics. J. Appl. Log. 4, 414–427 (2006).
Urban, J. MPTP 0.2: Design, Implementation, and Initial Experiments. J. Autom. Reasoning 37,
21–43 (2006).
Urban, J. MPTP - Motivation, Implementation, First Experiments. J. Autom. Reasoning 33, 319–
339 (2004).
Page 2 of 14

UrbanCV

27. Urban, J. MPTP 0.1: System Description. Electron. Notes Theor. Comput. Sci. 86, 147–152 (2003).
28. Urban, J. Order sorted algebras. Formalized Mathematics 10, 179–188 (2002).
29. Urban, J. Subalgebras of an order sorted algebra. Lattice of subalgebras. Formalized Mathematics
10, 189–196 (2002).
30. Urban, J. Homomorphisms of order sorted algebras. Formalized Mathematics 10, 197–200 (2002).
31. Urban, J. Order sorted quotient algebra. Formalized Mathematics 10, 201–210 (2002).
32. Urban, J. Free Order Sorted Universal Algebra. Formalized Mathematics 10, 211–225 (2002).
33. Urban, J. Mahlo and Inaccessible Cardinals. Formalized Mathematics 9, 485–490 (2001).
34. Urban, J. Basic facts about inaccessible and measurable cardinals. Formalized Mathematics 9, 323–
330 (2001).
Chapters in Collective Volumes as Main Author:

35.

Harrison, J., Urban, J. & Wiedijk, F. History of Interactive Theorem Proving in Computational
Logic (ed Siekmann, J. H.) 135–214 (Elsevier, 2014).
36. Urban, J. & Vyskocil, J. Theorem Proving in Large Formal Mathematics as an Emerging AI Field in
Automated Reasoning and Mathematics - Essays in Memory of William W. McCune (eds Bonacina,
M. P. & Stickel, M. E.) 240–257 (Springer, 2013).
37.

Urban, J., Vyskočil, J. & Štěpánek, P. Automatické uvažovánı́ (Automated Reasoning - in Czech)in Umělá inteligence (Artificial Intelligence - in Czech) (eds Mařı́k, V., Lažanský, J. & Štěpánková,O.) (Academia, Prague, 2013).

Papers in Proceedings:

38.

39.

40.

41.

42.

43.

44.
45.
46.

Goertzel, Z. A., Chvalovský, K., Jakubuv, J., Olsák, M. & Urban, J. Fast and Slow Enigmas andParental Guidance in Frontiers of Combining Systems - 13th International Symposium, FroCoS
2021, Birmingham, UK, September 8-10, 2021, Proceedings 12941 (Springer, 2021), 173–191.
Zhang, L., Blaauwbroek, L., Piotrowski, B., Cerný, P., Kaliszyk, C. & Urban, J. Online Machine Learning Techniques for Coq: A Comparison in Intelligent Computer Mathematics - 14th
International Conference, CICM 2021, Timisoara, Romania, July 26-31, 2021, Proceedings 12833(Springer, 2021), 67–83.
Macke, J., Sedlár, J., Olsák, M., Urban, J. & Sivic, J. Learning to Solve Geometric Construction
Problems from Images in Intelligent Computer Mathematics - 14th International Conference, CICM
2021, Timisoara, Romania, July 26-31, 2021, Proceedings 12833 (Springer, 2021), 167–184.
Zombori, Z., Csiszárik, A., Michalewski, H., Kaliszyk, C. & Urban, J. Towards Finding Longer Proofs
in Automated Reasoning with Analytic Tableaux and Related Methods - 30th International Conference, TABLEAUX 2021, Birmingham, UK, September 6-9, 2021, Proceedings 12842 (Springer,2021), 167–186.
Zombori, Z., Urban, J. & Olsák, M. The Role of Entropy in Guiding a Connection Prover in Automated Reasoning with Analytic Tableaux and Related Methods - 30th International Conference,
TABLEAUX 2021, Birmingham, UK, September 6-9, 2021, Proceedings 12842 (Springer, 2021),
218–235.
Chvalovský, K., Jakubuv, J., Olsák, M. & Urban, J. Learning Theorem Proving Components in
Automated Reasoning with Analytic Tableaux and Related Methods - 30th International Conference,
TABLEAUX 2021, Birmingham, UK, September 6-9, 2021, Proceedings 12842 (Springer, 2021),
266–278.
Jakubuv, J., Chvalovský, K., Olsák, M., Piotrowski, B., Suda, M. & Urban, J. ENIGMA Anonymous:
Symbol-Independent Inference Guiding Machine in IJCAR 2020 12167 (Springer, 2020), 448–463.
Zombori, Z., Urban, J. & Brown, C. E. Prolog Technology Reinforcement Learning Prover in IJCAR
2020 12167 (Springer, 2020), 489–507.
Wang, Q., Brown, C. E., Kaliszyk, C. & Urban, J. Exploration of neural machine translation in
autoformalization of mathematics in Mizar in CPP 2020 (ACM, 2020), 85–98.
Page 3 of 14

Urban
47.
48.
49.
50.
51.
52.
53.
54.
55.
56.
57.
58.
59.
60.
61.
62.
63.
64.
65.
66.
67.
68.
69.
70.
71.

CV
Blaauwbroek, L., Urban, J. & Geuvers, H. Tactic Learning and Proving for the Coq Proof Assistantin LPAR 2020 73 (EasyChair, 2020), 138–150.
Piotrowski, B. & Urban, J. Stateful Premise Selection by Recurrent Neural Networks in LPAR 2020
73 (EasyChair, 2020), 409–422.
Olsák, M., Kaliszyk, C. & Urban, J. Property Invariant Embedding for Automated Reasoning in
ECAI 2020 To appear. (2020).
Blaauwbroek, L., Urban, J. & Geuvers, H. The Tactician: A Seamless, Interactive Tactic Learnerand Prover for Coq in CICM 2020 To appear. (Springer, 2020).
Piotrowski, B. & Urban, J. Guiding Connection Tableau by Recurrent Neural Networks in CICM
2020 To appear. (Springer, 2020).
Urban, J. & Jakubuv, J. First Neural Conjecturing Datasets and Experiments in CICM 2020 To
appear. (Springer, 2020).
Brown, C. E., Gauthier, T., Kaliszyk, C., Sutcliffe, G. & Urban, J. GRUNGE: A Grand Unified
ATP Challenge in CADE 27 11716 (Springer, 2019), 123–141.
Chvalovský, K., Jakubuv, J., Suda, M. & Urban, J. ENIGMA-NG: Efficient Neural and GradientBoosted Inference Guidance for E in CADE 27 11716 (Springer, 2019), 197–215.
Jakubuv, J. & Urban, J. Hammering Mizar by Learning Clause Guidance (Short Paper) in ITP
2019 141 (Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2019), 34:1–34:8.
Goertzel, Z., Jakubuv, J. & Urban, J. ENIGMAWatch: ProofWatch Meets ENIGMA in TABLEAUX
2019 11714 (Springer, 2019), 374–388.
Piotrowski, B. & Urban, J. ATPBoost: Learning Premise Selection in Binary Setting with ATP
Feedback in IJCAR 2018 10900 (Springer, 2018), 566–574.
Goertzel, Z., Jakubuv, J., Schulz, S. & Urban, J. ProofWatch: Watchlist Guidance for Large Theories
in E in ITP 2018 10895 (Springer, 2018), 270–288.
Bancerek, G., Naumowicz, A. & Urban, J. System Description: XSL-Based Translator of Mizar to
LaTeX in CICM 2018 11006 (Springer, 2018), 1–6.
Jakubuv, J. & Urban, J. Enhancing ENIGMA Given Clause Guidance in CICM 2018 11006(Springer, 2018), 118–124.
Wang, Q., Kaliszyk, C. & Urban, J. First Experiments with Neural Translation of Informal to Formal
Mathematics in CICM 2018 11006 (Springer, 2018), 255–270.
Kaliszyk, C., Urban, J., Michalewski, H. & Olsák, M. Reinforcement Learning of Theorem Proving
in NeurIPS 2018 (2018), 8836–8847.
Goertzel, Z., Jakubuv, J. & Urban, J. ProofWatch Meets ENIGMA: First Experiments in LPAR-22
IWIL Workshop 9 (EasyChair, 2018), 15–22.
Urban, J. AI at CADE/IJCAR in ARCADE 2017 51 (EasyChair, 2017), 33–36.
Schulz, S., Sutcliffe, G., Urban, J. & Pease, A. Detecting Inconsistencies in Large First-Order Knowledge Bases in CADE 26 10395 (Springer, 2017), 310–325.
Färber, M., Kaliszyk, C. & Urban, J. Monte Carlo Tableau Proof Search in CADE 26 10395(Springer, 2017), 563–579.
Jakubuv, J. & Urban, J. BliStrTune: hierarchical invention of theorem proving strategies in CPP
2017 (ACM, 2017), 43–52.
Jakubuv, J., Suda, M. & Urban, J. Automated Invention of Strategies and Term Orderings for
Vampire in GCAI 2017 50 (EasyChair, 2017), 121–133.
Kaliszyk, C., Urban, J. & Vyskocil, J. Automating Formalization by Statistical and Semantic Parsingof Mathematics in ITP 2017 10499 (Springer, 2017), 12–27.
Gauthier, T., Kaliszyk, C. & Urban, J. TacticToe: Learning to Reason with HOL4 Tactics in LPAR
21 46 (EasyChair, 2017), 125–143.
Jakubuv, J. & Urban, J. ENIGMA: Efficient Learning-Based Inference Guiding Machine in CICM
2017 10383 (Springer, 2017), 292–302.
Page 4 of 14

UrbanCV

72.

Kaliszyk, C., Urban, J. & Vyskocil, J. System Description: Statistical Parsing of Informalized Mizar
Formulas in SYNASC 2017 (IEEE Computer Society, 2017), 169–172.
73. Kaliszyk, C., Pak, K. & Urban, J. Towards a Mizar environment for Isabelle: foundations andlanguage in CPP 2016 (ACM, 2016), 58–65.
74.
75.
76.
77.
78.
79.
80.
81.

Urban, J. Learning Intelligent Theorem Proving from Large Formal Corpora in ISAIM 2016 (2016).
Brown, C. E. & Urban, J. Extracting Higher-Order Goals from the Mizar Mathematical Library in
CICM 2016 9791 (Springer, 2016), 99–114.
Jakubuv, J. & Urban, J. Extending E Prover with Similarity Based Clause Selection Strategies in
CICM 2016 9791 (Springer, 2016), 151–156.
Irving, G., Szegedy, C., Alemi, A. A., Eén, N., Chollet, F. & Urban, J. DeepMath - Deep Sequence
Models for Premise Selection in NIPS 2016 (2016), 2235–2243.
Gauthier, T., Kaliszyk, C. & Urban, J. Initial Experiments with Statistical Conjecturing over Large
Formal Corpora in (CICM 2016 - Work in Progress Proceedings 1785 (CEUR-WS.org, 2016), 219–
228.
Kaliszyk, C., Schulz, S., Urban, J. & Vyskocil, J. System Description: E.T. 0.1 in CADE-25 9195
(Springer, 2015), 389–398.
Kaliszyk, C., Urban, J. & Vyskocil, J. Certified Connection Tableaux Proofs for HOL Light and
TPTP in CPP 2015 (ACM, 2015), 59–66.
Kaliszyk, C., Urban, J. & Vyskocil, J. Lemmatization for Stronger Reasoning in Large Theories in
FroCoS 2015 9322 (Springer, 2015), 341–356.

82. Urban, J. BliStr: The Blind Strategymaker in GCAI 2015 36 (EasyChair, 2015), 312–319.
83. Kaliszyk, C., Urban, J. & Vyskocil, J. Efficient Semantic Features for Automated Reasoning overLarge Theories in IJCAI 2015 (AAAI Press, 2015), 3084–3090.
84.
85.
86.
87.
88.
89.
90.
91.

92.
93.
94.
95.

Kaliszyk, C., Urban, J. & Vyskocil, J. Learning to Parse on Aligned Corpora (Rough Diamond) in
ITP 2015 9236 (Springer, 2015), 227–233.
Kaliszyk, C., Urban, J. & Vyskocil, J. Improving Statistical Linguistic Algorithms for Parsing Mathematics in IWIL@LPAR 2015 40 (EasyChair, 2015), 27–36.
Kaliszyk, C. & Urban, J. FEMaLeCoP: Fairly Efficient Machine Learning Connection Prover in
LPAR-20 9450 (Springer, 2015), 88–96.
Bancerek, G., Bylinski, C., Grabowski, A., Kornilowicz, A., Matuszewski, R., Naumowicz, A., Pak,
K. & Urban, J. Mizar: State-of-the-art and Beyond in CICM 2015 9150 (Springer, 2015), 261–279.
Kaliszyk, C., Urban, J., Siddique, U., Afshar, S. K., Dunchev, C. & Tahar, S. Formalizing Physics:
Automation, Presentation and Foundation Issues in CICM 2015 9150 (Springer, 2015), 288–295.
Urban, J. & Veroff, R. Experiments with State-of-the-art Automated Provers on Problems in Tarskian
Geometry in IWIL@LPAR 2015 40 (EasyChair, 2015), 122–126.
Kaliszyk, C., Urban, J. & Vyskocil, J. Machine Learner for Automated Reasoning 0.4 and 0.5 in
PAAR@IJCAR 2014 31 (EasyChair, 2014), 60–66.
Kaliszyk, C., Urban, J., Vyskocil, J. & Geuvers, H. Developing Corpus-Based Translation Methods
between Informal and Formal Mathematics: Project Description in CICM 2014 8543 (Springer,2014), 435–439.
Kaliszyk, C. & Urban, J. Wikis and Collaborative Systems for Large Formal Mathematics in SWCS
2013 and 2014 - Revised Selected and Invited Papers 9507 (Springer, 2014), 35–52.
Kaliszyk, C., Mamane, L. & Urban, J. Machine Learning of Coq Proof Guidance: First Experiments
in SCSS 2014 30 (EasyChair, 2014), 27–34.
Joosten, S. J. C., Kaliszyk, C. & Urban, J. Initial Experiments with TPTP-style Automated Theorem
Provers on ACL2 Problems in ACL2 - 12 152 (2014), 77–85.
Kaliszyk, C. & Urban, J. Stronger Automation for Flyspeck by Feature Weighting and Strategy
Evolution in PxTP 2013 14 (EasyChair, 2013), 87–95.

Page 5 of 14

Urban96.

CV
Kaliszyk, C. & Urban, J. PRocH: Proof Reconstruction for HOL Light in CADE-24 7898 (Springer,2013), 267–274.

97. Kühlwein, D., Schulz, S. & Urban, J. E-MaLeS 1.1 in CADE-24 7898 (Springer, 2013), 407–413.
98. Kühlwein, D., Blanchette, J. C., Kaliszyk, C. & Urban, J. MaSh: Machine Learning for Sledgehammer in ITP 2013 7998 (Springer, 2013), 35–50.
99. Tankink, C., Kaliszyk, C., Urban, J. & Geuvers, H. Communicating Formal Proofs: The Case of
Flyspeck in ITP 2013 7998 (Springer, 2013), 451–456.
100.
101.
102.
103.
104.
105.
106.
107.

108.
109.
110.
111.
112.
113.
114.
115.
116.

Kaliszyk, C. & Urban, J. Lemma Mining over HOL Light in LPAR-19 8312 (Springer, 2013), 503–
517.
Kaliszyk, C. & Urban, J. Automated Reasoning Service for HOL Light in CICM 2013 7961 (Springer,2013), 120–135.
Tankink, C., Kaliszyk, C., Urban, J. & Geuvers, H. Formal Mathematics on Display: A Wiki for
Flyspeck in CICM 2013 7961 (Springer, 2013), 152–167.
Alama, J., Mamane, L. & Urban, J. Dependencies in Formal Mathematics: Applications and Extraction for Coq and Mizar in CICM 2012 7362 (Springer, 2012), 1–16.
Tankink, C., Lange, C. & Urban, J. Point-and-Write - Documenting Formal Mathematics by Reference in CICM 2012 7362 (Springer, 2012), 169–185.
Kaliszyk, C. & Urban, J. Initial Experiments with External Provers and Premise Selection on HOL
Light Corpora in PAAR-2012 21 (EasyChair, 2012), 72–81.
Kühlwein, D. & Urban, J. Learning from Multiple Proofs: First Experiments in PAAR-2012 21(EasyChair, 2012), 82–94.
Kühlwein, D., van Laarhoven, T., Tsivtsivadze, E., Urban, J. & Heskes, T. Overview and Evaluationof Premise Selection Techniques for Large Theory Mathematics in IJCAR 2012 7364 (Springer,2012), 378–392.
Alama, J., Kühlwein, D. & Urban, J. Automated and Human Proofs in General Mathematics: An
Initial Comparison in LPAR-18 7180 (Springer, 2012), 37–45.
Urban, J. An Overview of Methods for Large-Theory Automated Theorem Proving in ATE 2011 760(CEUR-WS.org, 2011), 3–8.
Kühlwein, D., Urban, J., Tsivtsivadze, E., Geuvers, H. & Heskes, T. Multi-output Ranking for
Automated Reasoning in KDIR 2011 (SciTePress, 2011), 42–51.
Urban, J. Content-based encoding of mathematical and code libraries in ITP 2011 Workshop on
Mathematical Wikis 767 (CEUR-WS.org, 2011), 49–53.
Alama, J., Brink, K., Mamane, L. & Urban, J. Large Formal Wikis: Issues and Solutions in MKM
2011 6824 (Springer, 2011), 133–148.
Alama, J., Kohlhase, M., Mamane, L., Naumowicz, A., Rudnicki, P. & Urban, J. Licensing the Mizar
Mathematical Library in CICM 2011 6824 (Springer, 2011), 149–163.
Kühlwein, D., Urban, J., Tsivtsivadze, E., Geuvers, H. & Heskes, T. Learning2Reason in CICM
2011 6824 (Springer, 2011), 298–300.
Tsivtsivadze, E., Urban, J., Geuvers, H. & Heskes, T. Semantic Graph Kernels for AutomatedReasoning in SDM 2011 (SIAM / Omnipress, 2011), 795–803.
Urban, J., Vyskocil, J. & Stepánek, P. MaLeCoP Machine Learning Connection Prover in TABLEAUX
2011 6793 (Springer, 2011), 263–277.

117. Rudnicki, P. & Urban, J. Escape to ATP for Mizar in PxTP 2011 (2011).
118. Urban, J. & Sutcliffe, G. Automated Reasoning and Presentation Support for Formalizing Mathematics in Mizar in CICM 2010 6167 (Springer, 2010), 132–146.
119. Urban, J., Alama, J., Rudnicki, P. & Geuvers, H. A Wiki for Mizar: Motivation, Considerations,and Initial Prototype in CICM 2010 6167 (Springer, 2010), 455–469.
120. Urban, J., Hoder, K. & Voronkov, A. Evaluation of Automated Theorem Proving on the Mizar
Mathematical Library in ICMS 2010 6327 (Springer, 2010), 155–166.
Page 6 of 14

Urban
121.
122.
123.
124.
125.
126.
127.
128.

CV
Vyskocil, J., Stanovský, D. & Urban, J. Automated Proof Compression by Invention of New Definitions in LPAR-16 6355 (Springer, 2010), 447–462.
Urban, J., Sutcliffe, G., Pudlák, P. & Vyskocil, J. MaLARea SG1- Machine Learner for AutomatedReasoning with Semantic Guidance in IJCAR 2008 5195 (Springer, 2008), 441–456.
Urban, J. Automated Reasoning for Mizar: Artificial Intelligence through Knowledge Exchange in
LPAR 2008 Workshop on Knowledge Exchange 418 (CEUR-WS.org, 2008).
Urban, J. MaLARea: a Metasystem for Automated Reasoning in Large Theories in CADE-21 Workshop on Empirically Successful Automated Reasoning in Large Theories 257 (CEUR-WS.org, 2007).
Urban, J. & Sutcliffe, G. ATP Cross-Verification of the Mizar MPTP Challenge Problems in LPAR
2007 4790 (Springer, 2007), 546–560.
Urban, J. XML-izing Mizar: Making Semantic Processing and Presentation of MML Easy in MKM
2005 3863 (Springer, 2005), 346–360.
Bancerek, G. & Urban, J. Integrated Semantic Browsing of the Mizar Mathematical Library for
Authoring Mizar Articles in MKM 2004 3119 (Springer, 2004), 44–57.
Urban, J. Translating Mizar for First Order Theorem Provers in MKM 2003 2594 (Springer, 2003),
203–215.

Edited Volumes:

129.

Labahn, G., Davenport, J. & Urban, J. Special Issue on ICMS 2018. Mathematics in Computer
Science To appear (2020).
130. Fontaine, P., Kaliszyk, C., Schulz, S. & Urban, J. Special Issue on Automated Reasoning. AI Communications 31 (2018).
131.

(eds Konev, B., Urban, J. & Rümmer, P.) Proceedings of the 6th Workshop on Practical Aspects ofAutomated Reasoning co-located with Federated Logic Conference 2018 (FLoC 2018), Oxford, UK,
July 19th, 2018 2162 (CEUR-WS.org, 2018).

132.

(eds Davenport, J. H., Kauers, M., Labahn, G. & Urban, J.) Mathematical Software - ICMS 2018 6th International Conference, South Bend, IN, USA, July 24-27, 2018, Proceedings 10931 (Springer,2018).
133. J. R. Harrison, J. U. & Wiedijk, F. Special Issue on Twenty Years of the QED Manifesto. Journalof Formalized Reasoning 9 (2016).
134.

(eds Fontaine, P., Schulz, S. & Urban, J.) Proceedings of the 5th Workshop on Practical Aspects ofAutomated Reasoning 1635 (CEUR-WS.org, 2016).

135.

(eds Watt, S. M., Davenport, J. H., Sexton, A. P., Sojka, P. & Urban, J.) Intelligent Computer Mathematics - International Conference, CICM 2014, Coimbra, Portugal, July 7-11, 2014. Proceedings
8543 (Springer, 2014).

136.

(eds England, M. et al.) Joint Proceedings of the MathUI, OpenMath and ThEdu Workshops andWork in Progress track at CICM co-located with CICM 2014 1186 (CEUR-WS.org, 2014).

137.

(eds Blanchette, J. C. & Urban, J.) Proceedings of PxTP 2013 14 (EasyChair, 2013).

138.

(eds Davenport, J. H., Farmer, W. M., Urban, J. & Rabe, F.) Intelligent Computer Mathematics- 18th Symposium, Calculemus 2011, and 10th International Conference, MKM 2011, Bertinoro,
Italy, July 18-23, 2011. Proceedings 6824 (Springer, 2011).

139.

(eds Asperti, A., Davenport, J. H., Farmer, W. M., Urban, J. & Rabe, F.) Conference on Intelligent
Computer Mathematics 2011 - Work-in-Progress Papers Proceedings UBLCS-2011-04 (Universityof Bologna, 2011).

140.

(eds Lange, C. & Urban, J.) Proceedings of the ITP 2011 Workshop on Mathematical Wikis 767(CEUR-WS.org, 2011).

141.

(eds Sutcliffe, G., Urban, J. & Schulz, S.) Proceedings of CADE-21 Workshop on Empirically Successful Automated Reasoning in Large Theories, Bremen, Germany, 17th July 2007 257 (CEUR-WS.org,
2007).
Page 7 of 14

UrbanCV

Invited talks:
1. AI for Theorem Proving, OECD Workshop on AI and the Productivity of Science, 2-5/11/2021
2. Towards the Dream of Self-Improving Universal Reasoning AI, 14th Conference on Artificial GeneralIntelligence (AGI 2021), Palo Alto, 15-18/10/2021
3. Developments in AI and Theorem Proving, National Meeting of the Portuguese Mathematical Society
2021, 12-16/07/2021
4. Theorem Proving and Artificial Intelligence – A Brief Introduction, MATH-AI: ICLR’21 Workshop on
the Role of Mathematical Reasoning in General Artificial Intelligence, 7/05/2021
5. AI and Theorem Proving, New Technologies in Mathematics Seminar, Harvard University, 13/01/2021
6. Informal2Formal: Automating Formalization by Statistical and Semantic Parsing of Mathematics,
Hausdorff Center for Mathematics Workshop on Mathematical Language and Practical Type Theory,
Bonn, 1-4/02/2020
7. Machine Learning in Automated and Interactive Theorem Proving. The 22nd International Conferenceon Theory and Applications of Satisfiability Testing (SAT 22), Lisboa, Portugal, 7-12/07/2019
8. Combining Learning and Reasoning Over Large Formal Math Corpora, Dagstuhl Seminar Logic andLearning, Dagstuhl, Germany, 1-6/09/2019
9. Formal Proof and Machine Learning. ForMaL 2019 - DigiCosme Spring School on Formal Methods
and Machine Learning, Paris, France, 4-7/06/2019
10. Learning and Reasoning over Big Proof Corpora, Big Proof Workshop, Edinburgh, UK, 27-31/05/2019
11. Artificial Intelligence for Large-Scale Computer-Assisted Reasoning, ERC Conference on Frontier Research and Artificial Intelligence, Brussels, Belgium, 25-26/10/2018
12. Some ML Tasks in Theorem Proving, Dagstuhl Seminar Machine Learning and Formal Methods,
Dagstuhl, Germany, 27-31/08/2018
13. No One Shall Drive Us From the Semantic AI Paradise of Computer-Understandable Math and Science, 11th International Conference on Artificial General Intelligence (AGI 2018), Prague, Czechia,
22-25/08/2018
14. Kepler and Hales: Conjectures and Proofs, Dreams and Their Realization, From the Fundamental
Lemma to Discrete Geometry, to Formal Verification - a conference in honor of Thomas C. Hales on
the occasion of his 60th birthday (Hales60), Pittsburgh, USA, 18-22/06/2018
15. Machine Learning for Proof Automation and Formalization, 24th International Conference On Types
For Proofs And Programs (TYPES 2018), Braga, Portugal, 18-21/06/2018
16. Beyond Deduction, Dagstuhl Seminar Deduction Beyond First-Order Logic, Dagstuhl, Germany, 1015/09/2017
17. Learning-assisted Theorem Proving and Formalization, Workshop on Geometry and Computer Science,
Pescara, Italy, 8-10/02/2017
18. Artificial Intelligence and Theorem Proving, 25th Prague Computer Science Seminar, Prague, Czechia,
26/01/2017
19. Parsing Mathematics by Learning from Aligned Corpora and Theorem Proving, Dagstuhl Seminar
Universality of Proofs, Dagstuhl, Germany, 16-21/10/2016
20. Advances in Formal Mathematics, 4th Prague Gathering of Logicians, Prague, Czechia, 1213/02/2016
21. Learning Reasoning and Understanding in Mathematics, Semantic Representation of Mathematical
Knowledge, Fields Institute, Toronto, 3-5/02/2016
22. Learning Intelligent Theorem Proving from Large Formal Corpora, International Symposium on Artificial Intelligence and Mathematics (ISAIM’16), Fort Laudardale, 4-6/01/2016
23. Computer-Understandable Mathematics: Is It Coming?, 53rd Summer School on General Algebra andOrdered Sets, Srnı́, Czech Republic, 29/08-4/09, 2015.
24. Inductive and Deductive AI over Large Formal Libraries, Formalization of Mathematics in Proof Assistants, Institut Henri Poincaré, Paris, France, 5-9/05/2014

Page 8 of 14

UrbanCV

25. AI over Large Formal Knowledge Bases: The First Decade, ARW’2013, Dundee, UK, 11-12/04/2013
26. Theorem Proving over Mizar, Flyspeck and Isabelle, ADAM’2013, Albuquerque, USA, 6-8/06/2013
27. AI via/for Large Mathematical Knowledge Bases Dagstuhl Seminar 12271: AI meets Formal Software
Development, Leibniz Center for Informatics, Dagstuhl, Germany, 1-6/07/2012
28. An Overview of Methods for Large-Theory Automated Theory Proving, CADE23 Workshop on Automated Theory Engineering, Wroclaw, Poland, 31/07/2011
29. Large Formal Libraries: Birthplace of Strong AI?, Deduction Seminar: Deduction at Scale, Max-Planck
Institute for Informatics, Germany, 7-11/03/2011
30. Automated Reasoning over the Mizar Library, AMS Special Session on Formal Math. for Mathematicians: Developing Large Repositories of Advanced Mathematics, New Orleans, USA, 6-9/01/2011
31. Automation and AI Tools for Mizar, Symposium and General Assembly of Mizar Japan,Tokyo, 06/09/2010
32. AI Methods in Automated Reasoning, ISLA 2010, Hyderabad, India, 25-28/01/2010
33. Automated Reasoning for Mizar: AI through Knowledge Exchange, KEAPPA and IWIL, Qatar, 22/10/2008.
34. Accessing Mizar and its Semantics on the Web, ICMS’2006, Castro Urdiales, Spain, 1-3/09/2006.
Program Committees:
1. Artificial Intelligence and Theorem Proving - AITP, Aussois/online, 2022, PC co-chair
2. International Joint Conference on Artificial Intelligence - IJCAI, online, 2022, Reviewer
3. International Conference on Learning Representations - ICLR, online, 2022, Reviewer
4. Artificial Intelligence and Theorem Proving - AITP, Aussois/online, 2021, PC co-chair
5. International Conference on Machine Learning - ICML, online, 2021, Reviewer
6. Conference on Neural Information Processing Systems - NeurIPS, online, 2021, Reviewer
7. International Joint Conference on Artificial Intelligence - IJCAI, online, 2021, Reviewer
8. Interactive Theorem Proving - ITP, Rome/online, 2021, PC member
9. International Conference on Learning Representations - ICLR, online, 2021, Reviewer
10. International Conference on Automated Reasoning with Analytic Tableaux and Related Methods,
Birmingham, 2021, PC member
11. Proof eXchange for Theorem Proving - PxTP, online, 2021, PC member
12. Artificial Intelligence and Theorem Proving - AITP, Aussois, 2020, PC co-chair
13. International Joint Conference on Automated Reasoning - IJCAR, Paris, 2020, PC member
14. Conference on Neural Information Processing Systems - NeurIPS, Vancouver, 2020, Reviewer
15. International Joint Conference on Artificial Intelligence - IJCAI, Yokohama, 2020, Reviewer
16. Conferences on Intelligent Computer Mathematics - CICM, Bertinoro, 2020, PC member
17. International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, Timisoara,
2020, PC member
18. Artificial Intelligence and Theorem Proving, Obergurgl, 2019, PC co-chair
19. Interactive Theorem Proving - ITP, Portland, 2019, PC member
20. Conference on Neural Information Processing Systems - NeurIPS, Vancouver, 2019, Reviewer
21. International Conference on Automated Reasoning with Analytic Tableaux and Related Methods,
London, 2019, PC member
22. Formal Structures for Computation and Deduction, Dortmund, 2019, PC member
23. Formal Mathematics for Mathematicians, Prague, 2019, PC member
24. Proof eXchange for Theorem Proving, Natal, 2019, PC member
25. Automated Reasoning: Challenges, Applications, Directions, Exemplary Achievements, Natal, 2019,
PC member
26. International Congress on Mathematical Software, South Bend, 2018, PC co-chair
27. Artificial Intelligence and Theorem Proving, Aussois, 2018, PC co-chair
28. Practical aspects of automated reasoning, Oxford, 2018, PC co-chair
29. International Joint Conference on Automated Reasoning, Oxford, 2018, PC member
Page 9 of 14

UrbanCV

30. ACM SIGPLAN Conference on Certified Programs and Proofs, Los Angeles, 2018, PC member
31. Conferences on Intelligent Computer Mathematics, Hagenberg, 2018, PC member
32. International Conference on Artificial Intelligence and Symbolic Computation, Suzhou, 2018, PC member
33. Global Conference on Artificial Intelligence, Luxembourg City, 2018, PC member
34. Formal Mathematics for Mathematicians, Hagenberg, 2018, PC member
35. International Workshop on the Implementation of Logics, Awassa, 2018, PC member
36. Artificial Intelligence and Theorem Proving, Obergurgl, 2017, PC co-chair
37. Interactive Theorem Proving, Brasilia, 2017, PC member
38. International Conference on Automated Reasoning with Analytic Tableaux and Related Methods,
Brasilia, 2017, PC member
39. Conferences on Intelligent Computer Mathematics, Edinburgh, 2017, PC member
40. International Conference on Knowledge Engineering and Semantic Web, Szczecin, 2017, PC member
41. International Workshop on the Implementation of Logics, Brasilia, 2017, PC co-chair
42. Proof eXchange for Theorem Proving, Brasilia, 2017, PC member
43. Artificial Intelligence and Theorem Proving, Obergurgl, 2016, PC co-chair
44. Practical Aspects of Automated Reasoning, Coimbra, 2016, PC co-chair
45. International Joint Conference on Automated Reasoning, Coimbra, 2016, PC member
46. Conferences on Intelligent Computer Mathematics, Bialystok, 2016, PC member
47. First International Workshop on Hammers for Type Theories, Coimbra, 2016, PC member
48. Formal Mathematics for Mathematicians, Bialystok, 2016, PC member
49. International Workshop on the Implementation of Logics, Suva, 2015, PC member
50. Conferences on Intelligent Computer Mathematics, Washington DC, 2015, PC member
51. Proof Exchange for Theorem Provers, Berlin, 2015, PC member
52. Formal Mathematics for Mathematicians, Washington DC, 2015, PC member
53. 22nd Workshop on Logic, Language, Information and Computation, 2015, Bloomington, USA, PC
member
54. 2nd International Workshop about Sets and Tools, 2015, Oslo, Norway, PC member
55. Mathematical Knowledge Management, Coimbra, Portugal, 2014, PC chair
56. Twenty Years of the QED Manifesto, Vienna, 2014, PC co-chair
57. Symposium on Symbolic and Numeric Algorithms for Scientific Computing, Timisoara, 2014, PC
member
58. 3rd International Workshop on Semantic Web Collaborative Spaces, Trentino, Italy, 2014, PC member
59. International Symposium on Frontiers of Combining Systems, Nancy, 2013, PC member
60. Conferences on Intelligent Computer Mathematics, Bath, 2013, PC member
61. Proof Exchange for Theorem Provers, Lake Placid, 2013, PC co-chair
62. Knowledge Intensive Automated Reasoning, Lake Placid, 2013, PC member
63. Semantic Web Collaborative Spaces, Montpellier, 2013, PC member
64. Conferences on Intelligent Computer Mathematics, Bremen, 2012, PC member
65. User Interfaces for Theorem Provers, Bremen, 2012, PC member
66. Automated Theory eXploration, Manchester, 2012, PC member
67. Semantic Web Collaborative Spaces, Lyon, 2012, PC member
68. Conferences on Intelligent Computer Mathematics, Bertinoro, 2011, PC Chair of the Systems track
69. The ITP 2011 Workshop on Mathematical Wikis, Nijmegen, 2011, PC co-chair
70. Practical Aspects of Automated Reasoning, Edinburgh, 2010, PC member
71. Workshop on Mathematically Intelligent Proof Search, Paris, 2010, PC member
72. Mathematical Knowledge Management, Grand Bend, 2009, PC member
73. Knowledge Exchange: Automated Provers and Proof Assistants, Qatar, 2008, PC member
74. Practical Aspects of Automated Reasoning, Sydney, 2008, PC member
Page 10 of 14

UrbanCV

75. Empirically Successful Automated Reasoning for Mathematics, Birmingham, 2008, PC member
76. Programming Languages for Mechanized Mathematics, 2008, Birmingham, PC member
77. Empirically Successful Automated Reasoning in Large Theories, Bremen, 2007, PC co-chair
78. Programming Languages for Mechanized Mathematics, Hagenberg, 2007, PC member
Other Journal and Conference Activities:• Co-established and co-organized since 2016 the yearly conference on Artificial Intelligence and Theorem
Proving (AITP).
• Conference co-chair of CICM 2019.
• Special issue journal editing: Journal of Formalized Reasoning, AI Communications, Mathematics in
Computer Science.
• Journal editorial boards: Formalized Mathematics (since 2006), Central European J. of Computer
Science (2010-2017).
• Other journals reviewed for: J. of Automated Reasoning, Artificial Intelligence, Communication of
ACM, International J. on Artificial Intelligence Tools, Logical Methods in Computer Science, J. of
Logic and Computation, AI Communications, J. of Applied Logic, Mathematics in Computer Science,
J. of Symbolic Computation.
Prizes and awards: (All from the CADE ATP System Competition – CASC)1
1. CASC 2020: MaLARea 1st in LTB (demo), ENIGMA 2nd in FOF
2. CASC 2019: ENIGMA 2nd in FEW, MaLARea 3rd in LTB (demo)
3. LTB category of CASC 2018 : 1st place of Machine Learner for Automated Reasoning
4. CASC 2017 and 2015: MaLARea 2nd in LTB, 1st in MZR (2015), E.T. 3rd in SLH (2017)
5. LTB, HOL and MZR category of the CASC competition at the 2013 CADE Conference: 1st place ofthe MaLARea system
6. MZR category of the CASC competition at the 2012 Turing Centenary Conference (Manchester): mostproblems solved ans 2nd place by the MaLARea system (£1000), 3rd place of the PS-E system (£500).
7. FOF category of the same competition: 2nd place of the E-MaLeS system. (£1000)
8. FOF category of the CASC competition at IJCAR 2012: 2nd place of the E-MaLeS system.
9. FOF category of the 2011 CASC competition in Wroclaw: 3rd place of the E-MaLeS system
10. MZR category of the 2008 CASC competition in Sydney: 1st place of the MaLARea system
11. The Annual SUMO Reasoning Prizes at CASC (2008): 2nd place of the MaLARea system ($1000)
Selected Service Activities:• Head of the Artificial Intelligence Department at CIIRC-CTU (since 2021, 5 T/TT staff, 15 junior/senior researchers as of 2021)• Head of the Automatic Reasoning and Formal Methods Group at CIIRC-CTU (since 2018, 14 junior/senior researchers as of 2020)• Member of the Assembly of the Czech Institute of Informatics, Robotics, and Cybernetics (since 2016)• Member (since 2016) and Head (since 2020) of the Promotion Committee of the Czech Institute ofInformatics, Robotics, and Cybernetics• Extended Core Team member of CLAIRE2 - Confederation of Laboratories for Artificial Intelligence
Research in Europe (since 2019). Significant involvement in a number of activities for AI in EU.
• ELLIS Unit Prague member (ELLIS Fellow since 2020).
• Panel member at the Czech Science Foundation (2017-2020, reviewed ca. 100 proposals) .
• Panel member for the French National Research Agency 2019 AI Chairs program• Best Paper Award committee member for the IJCAI-JAIT journal in 2019-2021
1
2

www.tptp.org/CASC
https://claire-ai.org/

Page 11 of 14

UrbanCV• Advisory Board member of the Global Arena Research Institute3 (since 2019).
• Professional Societies: Association for Automated Reasoning, CLAIRE, ELLIS, AICZECHIA, International Congress on Mathematical Software (Advisory Board member since 2018), Association ofMizar Users (Head of the Licensing Committee), Mathematical Knowledge Management Interest Group(Trustee for years 2013-2016), Association for Computing Machinery’s Special Interest Group on Programming Languages.
Teaching: (Charles University in Prague, Radboud University Nijmegen, Czech Technical University)• Lectures: Machine Learning and Reasoning, Formal Mathematics and Proof Assistants, AutomatedReasoning and Theorem Proving, Formalization and Verification of Mathematics• Exercises: Propositional and Predicate Logic, Non-procedural Programming, Analyses of Algorithms• Seminars: Automated Theorem Proving, Automated Reasoning Seminar
Graduate student (co-)supervision:• Krystof Hoder, MS - Charles U. (finished as a part of PhD at U. of Manchester under A. Voronkov)• Ondrej Kuncar, MS/PhD - Charles U. (PhD finished at TU Munich under T. Nipkow)• Daniel Kuehlwein, PhD - RU Nijmegen, (co-)supervisors T. Heskes, H. Geuvers, E, Tsivtsivadze• Vladimir Sisma, PhD - Charles U. - did not finish• Wouter Geraedts, MS - RU Nijmegen, (co-)supervisors H. Geuvers, F. Wiedijk• Mark Adams, PhD - RU Nijmegen, (co-)supervisors H. Geuvers, F. Wiedijk, C. Kaliszyk (in progress)• Zarathustra Goertzel, PhD - CTU in Prague, (co-)supervisor J. Jakubuv (in progress)• Lasse Blaauwbroek, PhD - RU Nijmegen, (co-)supervisors H. Geuvers (in progress)• Yutaka Nagashima, PhD - CTU in Prague and U. of Innsbruck, (co-)supervisor C. Kaliszyk• Bartosz Piotrowski, PhD - U. of Warsaw, (co-)supervisor H. Michalewski (in progress)• Qingxiang Wang, PhD - CTU in Prague and U. of Innsbruck, (co-)supervisor C. Kaliszyk (in progress)• Filip Bartek, PhD - CTU in Prague, (co-)supervisor M. Suda (in progress)• Jelle Piepenbrock, PhD - RU Nijmegen, (co-)supervisors T. Heskes and M. Janota (in progress)• Liao Zhang, PhD - U. of Innsbruck, (co-)supervisor C. Kaliszyk, L. Blaauwbroek, H. Geuvers (inprogress)
Postdoc/researcher direct supervision:• Jan Jakubuv, CTU in Prague, 2015 - ongoing• Chad Brown, CTU in Prague, 2016 - ongoing• Karel Chvalovsky, CTU in Prague, 2017 - ongoing• Thibault Gauthier, CTU in Prague, 2018 - ongoing• Martin Suda, CTU in Prague, 2018 - ongoing
Other academic and educational activities:• Founded the ATP and ITP courses and seminar at Charles Univ. in Prague. Co-founded (with P.
Stepanek) the Prague Automated Reasoning Group.4 The group members and alumni include: J.
Vyskocil (CTU), J. Jakubuv (Heriot-Watt, CTU), M. Suda (MPI Saarbrucken, U. Manchester), P.
Pudlak (CTU, Google), M. Janota (UC Dublin, INESC-ID Lisboa, Microsoft Research), K. Hoder (U.
Manchester, Google), O. Kuncar (TU Munich), D. Stanovsky (Charles U.).
Languages:
Czech (native), English (fluent), Polish (fluent), German (advanced), Russian (advanced), French (intermed.)34

https://www.globari.org/iab
http://arg.ciirc.cvut.cz/

Page 12 of 14

UrbanCV

Selected Projects Implemented:• Efficient Learning-Based Inference Guiding Machine: (ENIGMA) efficient learning-based guidance for saturation-style ATPs such as E prover. Achieved 70% real-time (10s) improvement after
several proving/learning iterations on the Mizar/MPTP corpus over E in a single-strategy setting. As
of 2020, implements several neural, gradient boosting, and linear learning methods.
• Machine Learner for Automated Reasoning: (MaLARea) combining deductive ATP and counterexample finding with machine learning in a closed loop. The strongest existing meta-system for
automated reasoning with large amount of previous proof knowledge. Recent incarnations include
ATPBoost with B. Piotrowski.
• Machine/Reinforcement Learning Connection Prover and its variants: (MaLeCoP, FEMaLeCoP, MonteCoP, rlCoP, plCoP - with Jiri Vyskocil, C. Kaliszyk, M. Faerber, M. Olsak, H. Michalewski
and Z. Zombori) A family of connection tableaux provers using machine learning and reinforcement
learning from a large body of solved problems and successful proof decisions to guide the internal ATP
proof search process. rlCoP and plCoP implement MCTS-style guidance a la AlphaZero resulting inover 40% improvement over unguided leanCoP on a testing set.
• Autoformalization of Mathematics: (with C. Kaliszyk, J. Vyskocil and Q. Wang). First systems
combining statistical (PCFG, neural) parsing with strong semantic methods such as type checking andtheorem proving to automatically translate informal math to formal.
• HOL(y) Hammer: (with C. Kaliszyk) AI/ATP system proving conjectures over the Flyspeck corpus
by a number of inductive/deductive methods. The system uses 14 complementary learning/deductive
strategies in parallel to prove (as of April 2013) 47% of the Flyspeck theorems and lemmas fully
automatically.
• GRUNGE: A Grand Unified ATP Challenge: (with Chad E. Brown, Thibault Gauthier, Cezary
Kaliszyk, Geoff Sutcliffe). First learning-ready large ATP benchmark that spans practically all major
ATP formalisms (first-order, higher-order, typed, polymorphic). Allows comparing ATPs that use
different formalism and their collaboration in larger AI metasystems.
• Blind Strategymaker: (BliStr and its variants such as BliStrTune - with J. Jakubuv) evolves new
ATP strategies for classes of similar problems by interleaving fast low-time strategy iterative evolution
steps with high-time strategy evaluation and re-classification steps. 30 hours of such evolution improved
the E prover by 25% on the Mizar problems.
• MPTP: Mizar Problems for Theorem Proving. Project bringing the largest formal mathematicallibrary to the world of automated reasoning and related AI methods. Translation of Mizar logic andlibrary to first-order ATP formats, preserving completeness and correctness, and providing consistentnamespaces for symbols and theorems. That in turn allows machine learning from the proofs in thewhole library, and makes research in combined ATP/AI metasystems like MaLARea possible.
• MizAR: parallelized AI/ATP, verification, and presentation service for Mizar5 . Provides: article
verification, linked HTML presentation, AI/ATP solving and explanation of Mizar problems, lemmasuggestion. Proves (as of September 2013) 40% of the Mizar theorems and lemmas fully automatically.
• MPTP Challenge: Design and implementation (with G. Sutcliffe) of the first large-theory AI/ATP
benchmark6 . This gave rise to the Large Theory Batch division of the annual CASC ATP competition.
• Mizar, HOL Light, and Isabelle proof advisors: Used machine learning on the tens of thousandsof proofs in the large Mizar Mathematical Library to train a lemma-selection advisor. Similar work forHales’ proof of Jordan theorem in HOL, and for Isabelle (experimental). Combining the advisors with
ATP systems to provide strong methods for reasoning over large complex theories.
• MoMM: System using ATP indexing methods for fast interreduction of ca. one million mathematical
propositions, and for real-time retrieval of relevant information from that knowledge base. Integration
56

http://mizar.cs.ualberta.ca/~mptp/MizAR.html
http://www.tptp.org/MPTPChallenge/

Page 13 of 14

UrbanCV

into the Emacs authoring environment for Mizar, its use for real-time searching of the Mizar library.
• Formal mathematical wiki for Coq and Mizar: Wikis for collaborative editing, verification,versioning, and web-presentation of computer-verified mathematics. Ongoing NWO-funded project.7• E-MaLeS: Machine Learning of Strategies for E prover (with D. Kuhlwein and E. Tsivtsivadze). Usingmachine learning methods to find optimal strategies for the E ATP system. Ongoing project.
• MizarMode: Authoring environment for Mizar, used by the majority of Mizar authors. Integrates
number of proof assistance methods, searching and presentation tools, AI and ATP advisors.
• XML-ization of Mizar: XML-based re-implementation of Mizar internal format and datastructures.
Used by a number of projects to understand and link with Mizar.
• Otter2Mizar: Tool automatically translating the Otter and Prover9 proofs into Mizar. This allows
import of ATP proofs back to Mizar and their Mizar verification.
• Formalization of the theory of order sorted algebras: Developed order sorted algebras, theirsubalgebras, homomorphisms, quotient and free (term) algebras in Mizar.
• Formalization of the theory of large cardinals: Formal Mizar development including proofs thatmeasurable and Mahlo cardinals are inaccessible, and that inaccessible cardinals give a model of ZF.

7

http://mws.cs.ru.nl/mwiki/, http://mws.cs.ru.nl/cwiki/, www.fnds.cs.ru.nl/fndswiki/Research/MathWiki

Page 14 of 14