| A formal proof of the Kepler conjecture T Hales, M Adams, G Bauer, TD Dang, J Harrison, H Le Truong, ... Forum of mathematics, Pi 5, e2, 2017 | 483 | 2017 |
| Hammering towards QED JC Blanchette, C Kaliszyk, LC Paulson, J Urban Journal of Formalized Reasoning 9 (1), 101-148, 2016 | 231 | 2016 |
| Learning-assisted automated reasoning with Flyspeck C Kaliszyk, J Urban Journal of Automated Reasoning 53, 173-213, 2014 | 206 | 2014 |
| Deep network guided proof search S Loos, G Irving, C Szegedy, C Kaliszyk arXiv preprint arXiv:1701.06972, 2017 | 202 | 2017 |
| Reinforcement learning of theorem proving C Kaliszyk, J Urban, H Michalewski, M Olšák Advances in Neural Information Processing Systems 31, 2018 | 188 | 2018 |
| Mizar 40 for mizar 40 C Kaliszyk, J Urban Journal of Automated Reasoning 55 (3), 245-256, 2015 | 174 | 2015 |
| Hammer for Coq: Automation for dependent type theory Ł Czajka, C Kaliszyk Journal of automated reasoning 61, 423-453, 2018 | 168 | 2018 |
| HOL(y)Hammer: Online ATP Service for HOL Light C Kaliszyk, J Urban Mathematics in Computer Science 9, 5-22, 2015 | 117 | 2015 |
| Learning to Reason with HOL4 tactics T Gauthier, C Kaliszyk, J Urban arXiv preprint arXiv:1804.00595, 2018 | 115* | 2018 |
| MaSh: machine learning for Sledgehammer D Kühlwein, JC Blanchette, C Kaliszyk, J Urban Interactive Theorem Proving: 4th International Conference, ITP 2013, Rennes …, 2013 | 110 | 2013 |
| Holstep: A machine learning dataset for higher-order logic theorem proving C Kaliszyk, F Chollet, C Szegedy arXiv preprint arXiv:1703.00426, 2017 | 103 | 2017 |
| A learning-based fact selector for Isabelle/HOL JC Blanchette, D Greenaway, C Kaliszyk, D Kühlwein, J Urban Journal of Automated Reasoning 57, 219-244, 2016 | 80 | 2016 |
| FEMaLeCoP: Fairly efficient machine learning connection prover C Kaliszyk, J Urban Logic for Programming, Artificial Intelligence, and Reasoning: 20th …, 2015 | 78 | 2015 |
| Efficient semantic features for automated reasoning over large theories C Kaliszyk, J Urban, J Vyskocil Palo Alto: AAAI Press, 2015 | 77 | 2015 |
| TacticToe: learning to prove with tactics T Gauthier, C Kaliszyk, J Urban, R Kumar, M Norrish Journal of Automated Reasoning 65 (2), 257-286, 2021 | 69 | 2021 |
| Learning-assisted theorem proving with millions of lemmas C Kaliszyk, J Urban Journal of symbolic computation 69, 109-128, 2015 | 64 | 2015 |
| First experiments with neural translation of informal to formal mathematics Q Wang, C Kaliszyk, J Urban Intelligent Computer Mathematics: 11th International Conference, CICM 2018 …, 2018 | 62 | 2018 |
| Exploration of neural machine translation in autoformalization of mathematics in Mizar Q Wang, C Brown, C Kaliszyk, J Urban Proceedings of the 9th ACM SIGPLAN International Conference on Certified …, 2020 | 60 | 2020 |
| Property invariant embedding for automated reasoning M Olšák, C Kaliszyk, J Urban ECAI 2020, 1395-1402, 2020 | 59 | 2020 |
| General bindings and alpha-equivalence in Nominal Isabelle C Urban, C Kaliszyk Logical methods in computer science 8, 2012 | 57 | 2012 |
Josef UrbanDistinguished Researcher at Czech Technical University in PragueVerified email at cvut.cz