It's not hard to tie a deterministic process to any stream of output. The thing "hand waves" a proof and some other process exhaustively searches for either lean operations or some other math-manipulator operations that may create a real proof. The processes go back and forth. A proof is a verifiable string at the end of the day and this is better-than-pure-brute-strategy search strategy guided by heuristics from math literature.

I think someone asked here a bit ago whether other search strategies using OpenAI levels of compute have been tried and think the answer is no (even 3 hours of present GPU computer I think is vast compared to anything available 10 years ago, say).