Beagle as a HOL4 external ATP method. - Thibault Gauthier; Cezary Kaliszyk; Chantal Keller; Michael Norrish (PAAR@IJCAR, 2014)

Matching Concepts across HOL Libraries. - Thibault Gauthier; Cezary Kaliszyk (CICM, 2014)

Premise Selection and External Provers for HOL4. - Thibault Gauthier; Cezary Kaliszyk (CPP, 2015)

Sharing HOL4 and HOL Light Proof Knowledge. - Thibault Gauthier; Cezary Kaliszyk (LPAR, 2015)

Initial Experiments with Statistical Conjecturing over Large Formal Corpora. - Thibault Gauthier; Cezary Kaliszyk; Josef Urban (FM4M/MathUI/ThEdu/DP/WIP@CIKM, 2016)

TacticToe: Learning to Reason with HOL4 Tactics. - Thibault Gauthier; Cezary Kaliszyk; Josef Urban (LPAR, 2017)

Classification of Alignments Between Concepts of Formal Mathematical Systems. - Dennis Müller 001; Thibault Gauthier; Cezary Kaliszyk; Michael Kohlhase; Florian Rabe 001 (CICM, 2017)

Learning to Reason with HOL4 tactics. - Thibault Gauthier; Cezary Kaliszyk; Josef Urban (CoRR, 2018)

Learning to Prove with Tactics. - Thibault Gauthier; Cezary Kaliszyk; Josef Urban; Ramana Kumar; Michael Norrish (CoRR, 2018)

GRUNGE: A Grand Unified ATP Challenge. - Chad E. Brown; Thibault Gauthier; Cezary Kaliszyk; Geoff Sutcliffe; Josef Urban (CADE, 2019)

Deep Reinforcement Learning in HOL4. - Thibault Gauthier (CoRR, 2019)

Self-Learned Formula Synthesis in Set Theory. - Chad E. Brown; Thibault Gauthier (CoRR, 2019)

Aligning concepts across proof assistant libraries. - Thibault Gauthier; Cezary Kaliszyk (J. Symb. Comput., 2019)

Deep Reinforcement Learning for Synthesizing Functions in Higher-Order Logic. - Thibault Gauthier (LPAR, 2020)

Tree Neural Networks in HOL4. - Thibault Gauthier (CICM, 2020)

Learned Provability Likelihood for Tactical Search. - Thibault Gauthier (SCSS, 2021)

TacticToe: Learning to Prove with Tactics. - Thibault Gauthier; Cezary Kaliszyk; Josef Urban; Ramana Kumar; Michael Norrish (J. Autom. Reason., 2021)

Proofgold: Blockchain for Formal Methods. - Chad E. Brown; Cezary Kaliszyk; Thibault Gauthier; Josef Urban (FMBC@CAV, 2022)

Program Synthesis for the OEIS. - Thibault Gauthier (CoRR, 2022)

Learning Program Synthesis for Integer Sequences from Scratch. - Thibault Gauthier; Josef Urban (AAAI, 2023)

A Mathematical Benchmark for Inductive Theorem Provers. - Thibault Gauthier; Chad E. Brown; Mikolas Janota; Josef Urban (LPAR, 2023)

Alien coding. - Thibault Gauthier; Miroslav Olsák; Josef Urban (Int. J. Approx. Reason., 2023)

Learning Guided Automated Reasoning: A Brief Survey. - Lasse Blaauwbroek; David M. Cerna; Thibault Gauthier; Jan Jakubuv; Cezary Kaliszyk; Martin Suda 001; Josef Urban (Logics and Type Systems in Theory and Practice, 2024)

A Formal Proof of R(4, 5)=25. - Thibault Gauthier; Chad E. Brown (ITP, 2024)

Learning Conjecturing from Scratch. - Thibault Gauthier; Josef Urban (CADE, 2025)