Comment by astrange

Agents can generate formal proofs that are checked with an oracle like Lean and can run in a loop.