Reviews: Learning dynamic polynomial proofs

The work seems to instantiate the general setting of combining ML/RL with proof guidance. The instantiation however seems quite different from existing theorem provers and applied to an area typically not considered by the core ATP community. Perhaps the discussion of related work could mention and compare with theorem proving in algebra with ATPs such as Otter, Prover9, Waldmeister and E, and the work on their ML-based guidance. It is far from correct that ML-based guidance focuses on tactical systems. Most of the work so far has been done on tableau system and saturation-style systems (leanCoP/rlCoP, E/ENIGMA) that learn guidance of elementary inference rules in their calculi.