This work is interesting, but it doesn't seem to acknowledge a lot of the state-of-the-art work in this area. Possibly that's because much of it is done in Prog

This work is interesting, but it doesn't seem to acknowledge a lot of the state-of-the-art work in this area. Possibly that's because much of it is done in Programming Languages venues, as opposed to Machine Learning venues. It can also be hard to compare works because there are several proof languages that folks use (the big ones are Coq, Isabelle/HOL, and Lean), with mutually exclusive benchmark sets. However, the paper here cites CoqGym and Gamepad, ML-based proof synthesis works that work in the Coq language, but doesn't reference TacTok (https://dl.acm.org/doi/10.1145/3428299 https://dl.acm.org/doi/10.1145/3428299) or Proverbot9001 (http://proverbot9001.ucsd.edu/ http://proverbot9001.ucsd.edu/), both of which are later works which significantly improve accuracy and performance on the same language (and for CoqGym, the same benchmarks). Disclaimer: I'm the author of Proverbot9001.