  We present a comparison of several online machine learning techniques for
tactical learning and proving in the Coq proof assistant. This work builds on
top of Tactician, a plugin for Coq that learns from proofs written by the user
to synthesize new proofs. Learning happens in an online manner, meaning that
Tactician's machine learning model is updated immediately every time the user
performs a step in an interactive proof. This has important advantages compared
to the more studied offline learning systems: (1) it provides the user with a
seamless, interactive experience with Tactician and, (2) it takes advantage of
locality of proof similarity, which means that proofs similar to the current
proof are likely to be found close by. We implement two online methods, namely
approximate k-nearest neighbors based on locality sensitive hashing forests and
random decision forests. Additionally, we conduct experiments with gradient
boosted trees in an offline setting using XGBoost. We compare the relative
performance of Tactician using these three learning methods on Coq's standard
library.
