Tactic Learning and Proving for the Coq Proof Assistant. - Lasse Blaauwbroek; Josef Urban; Herman Geuvers (LPAR, 2020)

The Tactician - A Seamless, Interactive Tactic Learner and Prover for Coq. - Lasse Blaauwbroek; Josef Urban; Herman Geuvers (CICM, 2020)

The Tactician (extended version): A Seamless, Interactive Tactic Learner and Prover for Coq. - Lasse Blaauwbroek; Josef Urban; Herman Geuvers (CoRR, 2020)

Online Machine Learning Techniques for Coq: A Comparison. - Liao Zhang; Lasse Blaauwbroek; Bartosz Piotrowski; Prokop Cerný; Cezary Kaliszyk; Josef Urban (CICM, 2021)

Learning Proof Transformations and Its Applications in Interactive Theorem Proving. - Liao Zhang; Lasse Blaauwbroek; Cezary Kaliszyk; Josef Urban (FroCoS, 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)

Graph2Tac: Online Representation Learning of Formal Math Concepts. - Lasse Blaauwbroek; Mirek Olsák; Jason Rute; Fidel Ivan Schaposnik Massolo; Jelle Piepenbrock; Vasily Pestun (ICML, 2024)

Graph2Tac: Learning Hierarchical Representations of Math Concepts in Theorem proving. - Jason Rute; Miroslav Olsák; Lasse Blaauwbroek; Fidel Ivan Schaposnik Massolo; Jelle Piepenbrock; Vasily Pestun (CoRR, 2024)

The Tactician's Web of Large-Scale Formal Knowledge. - Lasse Blaauwbroek (CoRR, 2024)

Hashing Modulo Context-Sensitive 𝛼-Equivalence. - Lasse Blaauwbroek; Miroslav Olsák; Herman Geuvers (Proc. ACM Program. Lang., 2024)