| 2026 | ITP | 130k Lines of Formal Topology in Two Weeks: Simple and Cheap Autoformalization for Everyone? (Short Paper). | Josef Urban |
| 2025 | CADE | Learning Conjecturing from Scratch. | Thibault Gauthier, Josef Urban |
| 2024 | ECAI | Machine Learning for Quantifier Selection in cvc5. | Jan Jakubuv, Mikols Janota, Jelle Piepenbrock, Josef Urban |
| 2024 | FMCAD | Some Adventures in Learning Proving, Instantiation and Synthesis. | Josef Urban |
| 2024 | LPAR | First Experiments with Neural cvc5. | Jelle Piepenbrock, Mikolas Janota, Josef Urban, Jan Jakubuv |
| 2023 | AAAI | Learning Program Synthesis for Integer Sequences from Scratch. | Thibault Gauthier, Josef Urban |
| 2023 | ITP | Automated Theorem Proving for Metamath. | Mario Carneiro, Chad E. Brown, Josef Urban |
| 2023 | ITP | MizAR 60 for Mizar 50. | Jan Jakubuv, Karel Chvalovsk, Zarathustra Amadeus Goertzel, Cezary Kaliszyk, Mirek Olsk, Bartosz Piotrowski, Stephan Schulz, Martin Suda, Josef Urban |
| 2023 | LPAR | Guiding an Instantiation Prover with Graph Neural Networks. | Karel Chvalovsk, Konstantin Korovin, Jelle Piepenbrock, Josef Urban |
| 2023 | LPAR | A Mathematical Benchmark for Inductive Theorem Provers. | Thibault Gauthier, Chad E. Brown, Mikolas Janota, Josef Urban |
| 2022 | CADE | Guiding an Automated Theorem Prover with Neural Rewriting. | Jelle Piepenbrock, Tom Heskes, Mikols Janota, Josef Urban |
| 2022 | CAV | Proofgold: Blockchain for Formal Methods. | Chad E. Brown, Cezary Kaliszyk, Thibault Gauthier, Josef Urban |
| 2022 | ITP | The Isabelle ENIGMA. | Zarathustra Amadeus Goertzel, Jan Jakubuv, Cezary Kaliszyk, Miroslav Olsk, Jelle Piepenbrock, Josef Urban |
| 2021 | TABLEAUX | Learning Theorem Proving Components. | Karel Chvalovsk, Jan Jakubuv, Miroslav Olsk, Josef Urban |
| 2021 | TABLEAUX | Towards Finding Longer Proofs. | Zsolt Zombori, Adrin Csiszrik, Henryk Michalewski, Cezary Kaliszyk, Josef Urban |
| 2021 | TABLEAUX | The Role of Entropy in Guiding a Connection Prover. | Zsolt Zombori, Josef Urban, Miroslav Olsk |
| 2020 | CADE | ENIGMA Anonymous: Symbol-Independent Inference Guiding Machine (System Description). | Jan Jakubuv, Karel Chvalovsk, Miroslav Olsk, Bartosz Piotrowski, Martin Suda, Josef Urban |
| 2020 | CADE | Prolog Technology Reinforcement Learning Prover - (System Description). | Zsolt Zombori, Josef Urban, Chad E. Brown |
| 2020 | CPP | Exploration of neural machine translation in autoformalization of mathematics in Mizar. | Qingxiang Wang, Chad E. Brown, Cezary Kaliszyk, Josef Urban |
| 2020 | ECAI | Property Invariant Embedding for Automated Reasoning. | Miroslav Olsk, Cezary Kaliszyk, Josef Urban |
| 2020 | LPAR | Tactic Learning and Proving for the Coq Proof Assistant. | Lasse Blaauwbroek, Josef Urban, Herman Geuvers |
| 2020 | LPAR | Stateful Premise Selection by Recurrent Neural Networks. | Bartosz Piotrowski, Josef Urban |
| 2019 | CADE | GRUNGE: A Grand Unified ATP Challenge. | Chad E. Brown, Thibault Gauthier, Cezary Kaliszyk, Geoff Sutcliffe, Josef Urban |
| 2019 | CADE | ENIGMA-NG: Efficient Neural and Gradient-Boosted Inference Guidance for E. | Karel Chvalovsk, Jan Jakubuv, Martin Suda, Josef Urban |
| 2019 | ITP | Hammering Mizar by Learning Clause Guidance (Short Paper). | Jan Jakubuv, Josef Urban |
| 2019 | TABLEAUX | ENIGMAWatch: ProofWatch Meets ENIGMA. | Zarathustra Amadeus Goertzel, Jan Jakubuv, Josef Urban |
| 2018 | CADE | ATPboost: Learning Premise Selection in Binary Setting with ATP Feedback. | Bartosz Piotrowski, Josef Urban |
| 2018 | ITP | ProofWatch: Watchlist Guidance for Large Theories in E. | Zarathustra Amadeus Goertzel, Jan Jakubuv, Stephan Schulz, Josef Urban |
| 2018 | LPAR | ProofWatch Meets ENIGMA: First Experiments. | Zarathustra Amadeus Goertzel, Jan Jakubuv, Josef Urban |
| 2017 | CADE | Detecting Inconsistencies in Large First-Order Knowledge Bases. | Stephan Schulz, Geoff Sutcliffe, Josef Urban, Adam Pease |
| 2017 | CADE | Monte Carlo Tableau Proof Search. | Michael Frber, Cezary Kaliszyk, Josef Urban |
| 2017 | CADE | AI at CADE/IJCAR. | Josef Urban |
| 2017 | CPP | BliStrTune: hierarchical invention of theorem proving strategies. | Jan Jakubuv, Josef Urban |
| 2017 | ITP | Automating Formalization by Statistical and Semantic Parsing of Mathematics. | Cezary Kaliszyk, Josef Urban, Jir Vyskocil |
| 2017 | LPAR | TacticToe: Learning to Reason with HOL4 Tactics. | Thibault Gauthier, Cezary Kaliszyk, Josef Urban |
| 2017 | SYNASC | System Description: Statistical Parsing of Informalized Mizar Formulas. | Cezary Kaliszyk, Josef Urban, Jir Vyskocil |
| 2016 | CIKM | Initial Experiments with Statistical Conjecturing over Large Formal Corpora. | Thibault Gauthier, Cezary Kaliszyk, Josef Urban |
| 2016 | CPP | Towards a mizar environment for isabelle: foundations and language. | Cezary Kaliszyk, Karol Pak, Josef Urban |
| 2016 | ISAIM | Learning Intelligent Theorem Proving from Large Formal Corpora. | Josef Urban |
| 2015 | CADE | System Description: E.T. 0.1. | Cezary Kaliszyk, Stephan Schulz, Josef Urban, Jir Vyskocil |
| 2015 | CPP | Certified Connection Tableaux Proofs for HOL Light and TPTP. | Cezary Kaliszyk, Josef Urban, Jir Vyskocil |
| 2015 | IJCAI | Efficient Semantic Features for Automated Reasoning over Large Theories. | Cezary Kaliszyk, Josef Urban, Jir Vyskocil |
| 2015 | ITP | Learning to Parse on Aligned Corpora (Rough Diamond). | Cezary Kaliszyk, Josef Urban, Jir Vyskocil |
| 2015 | LPAR | FEMaLeCoP: Fairly Efficient Machine Learning Connection Prover. | Cezary Kaliszyk, Josef Urban |
| 2015 | LPAR | Improving Statistical Linguistic Algorithms for Parsing Mathematics. | Cezary Kaliszyk, Josef Urban, Jir Vyskocil |
| 2015 | LPAR | Experiments with State-of-the-art Automated Provers on Problems in Tarskian Geometry. | Josef Urban, Robert Veroff |
| 2014 | CADE | Machine Learner for Automated Reasoning 0.4 and 0.5. | Cezary Kaliszyk, Josef Urban, Jir Vyskocil |
| 2013 | CADE | PRocH: Proof Reconstruction for HOL Light. | Cezary Kaliszyk, Josef Urban |
| 2013 | CADE | Stronger Automation for Flyspeck by Feature Weighting and Strategy Evolution. | Cezary Kaliszyk, Josef Urban |
| 2013 | CADE | E-MaLeS 1.1. | Daniel Khlwein, Stephan Schulz, Josef Urban |
| 2013 | ITP | MaSh: Machine Learning for Sledgehammer. | Daniel Khlwein, Jasmin Christian Blanchette, Cezary Kaliszyk, Josef Urban |
| 2013 | ITP | Communicating Formal Proofs: The Case of Flyspeck. | Carst Tankink, Cezary Kaliszyk, Josef Urban, Herman Geuvers |
| 2013 | LPAR | Lemma Mining over HOL Light. | Cezary Kaliszyk, Josef Urban |
| 2012 | AISC | Dependencies in Formal Mathematics: Applications and Extraction for Coq and Mizar. | Jesse Alama, Lionel Mamane, Josef Urban |
| 2012 | AISC | Point-and-Write - Documenting Formal Mathematics by Reference. | Carst Tankink, Christoph Lange, Josef Urban |
| 2012 | CADE | Initial Experiments with External Provers and Premise Selection on HOL Light Corpora. | Cezary Kaliszyk, Josef Urban |
| 2012 | CADE | Overview and Evaluation of Premise Selection Techniques for Large Theory Mathematics. | Daniel Khlwein, Twan van Laarhoven, Evgeni Tsivtsivadze, Josef Urban, Tom Heskes |
| 2012 | CADE | Learning from Multiple Proofs: First Experiments. | Daniel Khlwein, Josef Urban |
| 2012 | LPAR | Automated and Human Proofs in General Mathematics: An Initial Comparison. | Jesse Alama, Daniel Khlwein, Josef Urban |
| 2011 | IC3K | Multi-output Ranking for Automated Reasoning. | Daniel Khlwein, Josef Urban, Evgeni Tsivtsivadze, Herman Geuvers, Tom Heskes |
| 2011 | ITP | Content-based encoding of mathematical and code libraries. | Josef Urban |
| 2011 | SDM | Semantic Graph Kernels for Automated Reasoning. | Evgeni Tsivtsivadze, Josef Urban, Herman Geuvers, Tom Heskes |
| 2011 | TABLEAUX | MaLeCoP Machine Learning Connection Prover. | Josef Urban, Jir Vyskocil, Petr Stepnek |
| 2010 | AISC | A Wiki for Mizar: Motivation, Considerations, and Initial Prototype. | Josef Urban, Jesse Alama, Piotr Rudnicki, Herman Geuvers |
| 2010 | AISC | Automated Reasoning and Presentation Support for Formalizing Mathematics in Mizar. | Josef Urban, Geoff Sutcliffe |
| 2010 | LPAR | Automated Proof Compression by Invention of New Definitions. | Jir Vyskocil, David Stanovsk, Josef Urban |
| 2008 | CADE | MaLARea SG1- Machine Learner for Automated Reasoning with Semantic Guidance. | Josef Urban, Geoff Sutcliffe, Petr Pudlk, Jir Vyskocil |
| 2008 | LPAR | Automated Reasoning for Mizar: Artificial Intelligence through Knowledge Exchange. | Josef Urban |
| 2007 | CADE | MaLARea: a Metasystem for Automated Reasoning in Large Theories. | Josef Urban |
| 2007 | LPAR | ATP Cross-Verification of the Mizar MPTP Challenge Problems. | Josef Urban, Geoff Sutcliffe |
| 2000 | PIMRC | Broadband Radio Access for IP-based networks (BRAIN)-a key enabler for mobile Internet access. | Dave Wisely, Werner Mohr, Josef Urban |