It depends on what theory you're working in (at which point deciding whether to use one theory or another becomes more like a phisolophical question).

I'm mostly familiar with type theory, of which there are many variants, but the most common ones all share the most important characteristics. In particular they identify theorems with types, and proofs with terms, where correct proofs are well-typed terms. The nice thing is that terms are recursively enumerable, so you can list all proofs. Moreover most type theories have decidable type checking, so you can automatically check whether a terms if well-typed (and hence the corresponding proof is correct).

This is not just theory, there exist already a bunch of tools that are being used in practice for mechanically checking mathematical proofs, like Coq, Lean, Agda and more.

When I said "in theory" however it's because in practice enumerating all proof terms will be very very slow and will take forever to reach proofs for theorems that we might find interesting.

Since we're in the LLM topic, there are efforts to use LLMs to speed up this search, though this is more similar to using them as search heuristics though. It does help though that you can have automatic feedback thanks to the aforementioned proof checking tools, meaning you don't need costly human supervision to train them. The hope would be getting something like what Stockfish/Alphazero is for chess.