Lasse Blaauwbroek

Tactic Learning and Proving for the Coq Proof Assistant

2020 · EPiC series in computing

We present a system that utilizes machine learning for tactic proof search in the Coq Proof Assistant. In a similar vein as the TacticToe project for HOL4, our system predicts appropriate tactics and finds proofs …

The Tactician's Web of Large-Scale Formal Knowledge

2024 · arXiv (Cornell University)

The Tactician's Web is a platform offering a large web of strongly interconnected, machine-checked, formal mathematical knowledge conveniently packaged for machine learning, analytics, and proof engineering. Built on top of the Coq proof assistant, the …