Thesis directions in ML4TP

Stream: Machine Learning for Theorem Proving

[Gerben Koopman]

Hi, I got into Lean and ATP by working on a tree-search Lean project inspired by AlphaZero and the LeanDojo gym environment. Since then, AlphaProof has been released in more detail #Machine Learning for Theorem Proving > AlphaProof Paper (discussion)) and so I'm hoping to continue in this or other topics of ML4TP that are not subsumed to superior research by DeepMind.

Having been following this channel for a while now, I am inspired by some of the advances made, but I'm having a hard time formulating new research questions (which are also of a suitably small scale). One interesting avenue might be to explore hyperbolic LMs or RL agents (https://arxiv.org/pdf/2401.02949, https://arxiv.org/pdf/2210.01542) given Mathlib's hierarchical structure (ditto for math in general), but I would love to hear people's insights into the current state and potential future of AI usable to mathematicians.