🧑‍🔬 Josef Urban

🏛️ Affiliations

🎓Chalmers University of TechnologyGothenburg · Sweden2026 · 2 paperscurrent🎓University of GothenburgGothenburg · Sweden2026 · 2 paperscurrent🎓Czech Technical University in PraguePrague · Czechia2014–2025 · 72 papers🎓Radboud University NijmegenNijmegen · Netherlands2010–2018 · 65 papers🎓Charles UniversityPrague · Czechia2003–2008 · 12 papers🎓Universität InnsbruckInnsbruck · Austria2012–2018 · 7 papers

From the bylines of their papers (OpenAlex, 2026-10-14), ORCID and Wikidata; institutions on papers are matched by machine. 1 more institution on single bylines are not listed.

🧭 Fields, topics and concepts

Of its works in our library, with the number of works on each.

📅 Works by year

2010s

📄 Papers

The most cited first (OpenAlex and our library).

1. Learning-Assisted Automated Reasoning with Flyspeck (2012 · 165 citations)
   The paper addresses the lack of a "hammer" for HOL Light: a tool that automatically proves a new goal by choosing relevant lemmas from a large library and handing them to external automated theorem provers (ATPs).
2. Hammering towards QED (2016 · 127 citations)
   This survey covers "hammers," tools that let users of proof assistants prove hard lemmas automatically. The user does not have to script the proof search by hand. The tools draw on very large formal libraries, and the name comes from Sledgehammer for Isabelle and HOLyHammer for HOL Light.

All works

21 works of theirs in our library, the most cited first; 2 with a page here, the others link their original until we summarise them.

1. DeepMath - Deep Sequence Models for Premise Selection ↗arXiv:1606.04442 · no summary yetAlex A. Alemi et al.2016 · 178 citations
2. Learning-Assisted Automated Reasoning with FlyspeckarXiv:1211.7012 (J. Automated Reasoninig 54(1): 99, 2014)Cezary Kaliszyk, Josef Urban2012 · 165 citations
3. Premise Selection for Mathematics by Corpus Analysis and Kernel Methods ↗arXiv:1108.3446 · no summary yetJesse Alama et al.2011 · 152 citations
4. Hammering towards QEDJournal of Formalized Reasoning 9(1)Jasmin Christian Blanchette, Cezary Kaliszyk, Lawrence C. Paulson, et al.2016 · 127 citations
5. MizAR 40 for Mizar 40 ↗arXiv:1310.2805 (J. Automated Reasoning 55(3): 245-256 (2015)) · no summary yetCezary Kaliszyk, Josef Urban2013 · 112 citations
6. History of Interactive Theorem Proving ↗Handbook of the History of Logic, vol. 9 (Elsevier) · no summary yetJohn Harrison, Josef Urban, Freek Wiedijk2014 · 109 citations
7. A formal proof of the Kepler conjecture ↗arXiv:1501.02155 · no summary yetThomas Hales et al.2015 · 79 citations
8. ENIGMA: Efficient Learning-based Inference Guiding Machine ↗arXiv:1701.06532 · no summary yetJan Jakubův, Josef Urban2017 · 67 citations
9. First Experiments with Neural Translation of Informal to Formal Mathematics ↗arXiv:1805.06502 · no summary yetQingxiang Wang, Cezary Kaliszyk, Josef Urban2018 · 66 citations
10. ENIGMA-NG: Efficient Neural and Gradient-Boosted Inference Guidance for E ↗arXiv:1903.03182 · no summary yetKarel Chvalovský et al.2019 · 61 citations
11. TacticToe: Learning to Prove with Tactics ↗arXiv:1804.00596 (J. Automated Reasoning 65(2): 257-286, 2021) · no summary yetThibault Gauthier et al.2018 · 57 citations
12. MaLARea: a Metasystem for Automated Reasoning in Large Theories ↗ESARLT 2007, CEUR-WS Vol-257 · no summary yetJosef Urban2007 · 52 citations
13. Exploration of Neural Machine Translation in Autoformalization of Mathematics in Mizar ↗arXiv:1912.02636 · no summary yetQingxiang Wang et al.2019 · 50 citations
14. Reinforcement Learning of Theorem Proving ↗arXiv:1805.07563 · no summary yetCezary Kaliszyk et al.2018 · 50 citations
15. ENIGMA Anonymous: Symbol-Independent Inference Guiding Machine (system description) ↗arXiv:2002.05406 · no summary yetJan Jakubův et al.2020 · 42 citations
16. First Neural Conjecturing Datasets and Experiments ↗arXiv:2005.14664 · no summary yetJosef Urban, Jan Jakubův2020 · 40 citations
17. Property Invariant Embedding for Automated Reasoning ↗arXiv:1911.12073 (ECAI 2020 - 24th European Conference on Artificial Intelligence) · no summary yetMiroslav Olšák, Cezary Kaliszyk, Josef Urban2019 · 30 citations
18. Stateful Premise Selection by Recurrent Neural Networks ↗arXiv:2004.08212 · no summary yetBartosz Piotrowski, Josef Urban2020 · 21 citations
19. Towards Finding Longer Proofs ↗arXiv:1905.13100 · no summary yetZsolt Zombori et al.2019 · 21 citations
20. Guiding Inferences in Connection Tableau by Recurrent Neural Networks ↗arXiv:1905.07961 · no summary yetBartosz Piotrowski, Josef Urban2019 · 15 citations
21. HOL(y)Hammer: Online ATP Service for HOL Light ↗arXiv:1309.4962 · no summary yetCezary Kaliszyk, Josef Urban2013 · 13 citations

🤝 Co-authors here

1 co-author with a page, the most papers together first.

• Cezary Kaliszyk ×2

Venues

Where their works here were published, the most works first, with the editions of those that have a page.

• ESARLT 2007, CEUR-WS Vol-257
• Handbook of the History of Logic, vol. 9 (Elsevier)
• Journal of Formalized Reasoning 9(1)

🔗 Cited by

Papers of our library cite their works 417 times (of the 149,439 papers whose bibliographies we read); 18 citing papers with a page here →.

Updated 30 October 2026

↑ back to top

This page in Markdown → https://md.research.elamur.ai/free/en/authors/josef-urban/