| 2025 | CADE | Learning Conjecturing from Scratch. | Thibault Gauthier, Josef Urban |
| 2024 | ITP | A Formal Proof of R(4, 5)=25. | Thibault Gauthier, Chad E. Brown |
| 2023 | AAAI | Learning Program Synthesis for Integer Sequences from Scratch. | Thibault Gauthier, Josef Urban |
| 2023 | LPAR | A Mathematical Benchmark for Inductive Theorem Provers. | Thibault Gauthier, Chad E. Brown, Mikolas Janota, Josef Urban |
| 2022 | CAV | Proofgold: Blockchain for Formal Methods. | Chad E. Brown, Cezary Kaliszyk, Thibault Gauthier, Josef Urban |
| 2020 | LPAR | Deep Reinforcement Learning for Synthesizing Functions in Higher-Order Logic. | Thibault Gauthier |
| 2019 | CADE | GRUNGE: A Grand Unified ATP Challenge. | Chad E. Brown, Thibault Gauthier, Cezary Kaliszyk, Geoff Sutcliffe, Josef Urban |
| 2017 | LPAR | TacticToe: Learning to Reason with HOL4 Tactics. | Thibault Gauthier, Cezary Kaliszyk, Josef Urban |
| 2016 | CIKM | Initial Experiments with Statistical Conjecturing over Large Formal Corpora. | Thibault Gauthier, Cezary Kaliszyk, Josef Urban |
| 2015 | CPP | Premise Selection and External Provers for HOL4. | Thibault Gauthier, Cezary Kaliszyk |
| 2015 | LPAR | Sharing HOL4 and HOL Light Proof Knowledge. | Thibault Gauthier, Cezary Kaliszyk |
| 2014 | CADE | Beagle as a HOL4 external ATP method. | Thibault Gauthier, Cezary Kaliszyk, Chantal Keller, Michael Norrish |