Comment by c7b

With formalized math, you only need to validate the problem statement (in theory, in practice agents have already managed to exploit Lean compiler bugs, but the incidence of those should decrease enough to be practically lusable for 'blind' validation of AI proofs in the foreseeable future).