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 | 460 | 2017 |
Deepmath-deep sequence models for premise selection G Irving, C Szegedy, AA Alemi, N Eén, F Chollet, J Urban Advances in neural information processing systems 29, 2016 | 274* | 2016 |
Mizar: State-of-the-art and beyond G Bancerek, C Byliński, A Grabowski, A Korniłowicz, R Matuszewski, ... International Conference on Intelligent Computer Mathematics, 261-279, 2015 | 264 | 2015 |
Hammering towards QED JC Blanchette, C Kaliszyk, LC Paulson, J Urban Journal of Formalized Reasoning 9 (1), 101-148, 2016 | 226 | 2016 |
Learning-assisted automated reasoning with Flyspeck C Kaliszyk, J Urban Journal of Automated Reasoning 53, 173-213, 2014 | 202 | 2014 |
Reinforcement learning of theorem proving C Kaliszyk, J Urban, H Michalewski, M Olšák Advances in Neural Information Processing Systems 31, 2018 | 184 | 2018 |
Premise selection for mathematics by corpus analysis and kernel methods J Alama, T Heskes, D Kühlwein, E Tsivtsivadze, J Urban Journal of automated reasoning 52, 191-213, 2014 | 172 | 2014 |
Mizar 40 for mizar 40 C Kaliszyk, J Urban Journal of Automated Reasoning 55 (3), 245-256, 2015 | 171 | 2015 |
MPTP 0.2: Design, implementation, and initial experiments J Urban Journal of Automated Reasoning 37, 21-43, 2006 | 169 | 2006 |
MaLARea SG1-machine learner for automated reasoning with semantic guidance J Urban, G Sutcliffe, P Pudlák, J Vyskočil International Joint Conference on Automated Reasoning, 441-456, 2008 | 167 | 2008 |
History of interactive theorem proving J Harrison, J Urban, F Wiedijk Handbook of the History of Logic 9, 135-214, 2014 | 125 | 2014 |
Learning to reason with hol4 tactics T Gauthier, C Kaliszyk, J Urban arXiv preprint arXiv:1804.00595, 2018 | 114* | 2018 |
HOL(y)Hammer: Online ATP Service for HOL Light C Kaliszyk, J Urban Mathematics in Computer Science 9, 5-22, 2015 | 112 | 2015 |
MaSh: machine learning for Sledgehammer D Kühlwein, JC Blanchette, C Kaliszyk, J Urban Interactive Theorem Proving: 4th International Conference, ITP 2013, Rennes …, 2013 | 108 | 2013 |
ENIGMA: efficient learning-based inference guiding machine J Jakubův, J Urban Intelligent Computer Mathematics: 10th International Conference, CICM 2017 …, 2017 | 106 | 2017 |
MaLeCoP machine learning connection prover J Urban, J Vyskočil, P Štěpánek International Conference on Automated Reasoning with Analytic Tableaux and …, 2011 | 95 | 2011 |
XML-izing Mizar: making semantic processing and presentation of MML easy J Urban International Conference on Mathematical Knowledge Management, 346-360, 2005 | 88 | 2005 |
MPTP–motivation, implementation, first experiments J Urban Journal of Automated Reasoning 33, 319-339, 2004 | 88 | 2004 |
Overview and evaluation of premise selection techniques for large theory mathematics D Kühlwein, T van Laarhoven, E Tsivtsivadze, J Urban, T Heskes Automated Reasoning: 6th International Joint Conference, IJCAR 2012 …, 2012 | 87 | 2012 |
ATP and presentation service for Mizar formalizations J Urban, P Rudnicki, G Sutcliffe Journal of Automated Reasoning 50 (2), 229-241, 2013 | 85 | 2013 |