Yes, although they may not be ideal unless you're able to define a "distance" between a proof that the agent is proposing and whether that proof is correct (i.e

Yes, although they may not be ideal unless you're able to define a "distance" between a proof that the agent is proposing and whether that proof is correct (i.e. unless you're able to define a reward or energy function). It may be possible to infer/learn a score from existing proofs though. We have a paper that manages to both learn a flow and an energy function (the score) from data: https://arxiv.org/abs/2202.01361 https://arxiv.org/abs/2202.01361 I don't know much about theorem proving though. Can some value be attributed to partial proofs?