[riku_iki]

I think they can use transformer in the same way for proof path generation: do pattern matching for complex logical statements to find those where specific rule can be applied, similarly as it has be done in differential equations paper.

[Tainnor]

How does that help and/or address any of what I wrote?

You can generate possible transformations from one proposition to another one, yes. But the space of possible transformations is infinite, how does the system know which ones to try? Moreover, even if you try some local transformation, how do you know that you have made progress?

A system like that could probably perform well on typical undergraduate proofs: epsilon-delta, proof that such and such a thing is a norm, etc., but it's gonna have a hard time with more difficult problems.