| Learning to reason with hol4 tactics T Gauthier, C Kaliszyk, J Urban arXiv preprint arXiv:1804.00595, 2018 | 120* | 2018 |
| 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 | 72 | 2021 |
| Premise selection and external provers for HOL4 T Gauthier, C Kaliszyk Proceedings of the 2015 Conference on Certified Programs and Proofs, 49-57, 2015 | 51 | 2015 |
| Matching concepts across HOL libraries T Gauthier, C Kaliszyk International Conference on Intelligent Computer Mathematics, 267-281, 2014 | 43 | 2014 |
| Classification of alignments between concepts of formal mathematical systems D Müller, T Gauthier, C Kaliszyk, M Kohlhase, F Rabe International Conference on Intelligent Computer Mathematics, 83-98, 2017 | 34 | 2017 |
| Sharing HOL4 and HOL Light proof knowledge T Gauthier, C Kaliszyk Logic for Programming, Artificial Intelligence, and Reasoning: 20th …, 2015 | 31 | 2015 |
| Initial Experiments with Statistical Conjecturing over Large Formal Corpora. T Gauthier, C Kaliszyk, J Urban FM4M/MathUI/ThEdu/DP/WIP@ CIKM, 219-228, 2016 | 28 | 2016 |
| Aligning concepts across proof assistant libraries T Gauthier, C Kaliszyk Journal of Symbolic Computation 90, 89-123, 2019 | 23 | 2019 |
| Deep reinforcement learning for synthesizing functions in higher-order logic T Gauthier arXiv preprint arXiv:1910.11797, 2019 | 22 | 2019 |
| GRUNGE: A grand unified ATP challenge CE Brown, T Gauthier, C Kaliszyk, G Sutcliffe, J Urban Automated Deduction–CADE 27: 27th International Conference on Automated …, 2019 | 22 | 2019 |
| Alien coding T Gauthier, M Olšák, J Urban International Journal of Approximate Reasoning 162, 109009, 2023 | 9 | 2023 |
| Tree neural networks in HOL4 T Gauthier International Conference on Intelligent Computer Mathematics, 278-283, 2020 | 9 | 2020 |
| Self-learned formula synthesis in set theory CE Brown, T Gauthier arXiv preprint arXiv:1912.01525, 2019 | 6 | 2019 |
| Deep reinforcement learning in HOL4 T Gauthier CoRR, abs/1910.11797, 2019 | 6 | 2019 |
| Learning program synthesis for integer sequences from scratch T Gauthier, J Urban Proceedings of the AAAI Conference on Artificial Intelligence 37 (6), 7670-7677, 2023 | 5 | 2023 |
| Learning guided automated reasoning: a brief survey L Blaauwbroek, DM Cerna, T Gauthier, J Jakubův, C Kaliszyk, M Suda, ... Logics and Type Systems in Theory and Practice: Essays Dedicated to Herman …, 2024 | 4 | 2024 |
| A formal proof of R (4, 5)= 25 T Gauthier, CE Brown arXiv preprint arXiv:2404.01761, 2024 | 4 | 2024 |
| Beagle as a HOL4 external ATP method T Gauthier, C Kaliszyk, C Keller, M Norrish PAAR-Fourth Workshop on Practical Aspects of Automated Reasoning, 2014 | 4 | 2014 |
| Proofgold: Blockchain for formal methods CE Brown, C Kaliszyk, T Gauthier, J Urban 4th International Workshop on Formal Methods for Blockchains (FMBC 2022), 4 …, 2022 | 3 | 2022 |
| A mathematical benchmark for inductive theorem provers T Gauthier, CE Brown, M Janota, J Urban arXiv preprint arXiv:2304.02986, 2023 | 2 | 2023 |
