Are you sure? If an AI would generate a huge Lean proof/program, wouldn't there be a way to hide such cheats in it? Like as in the underhanded C contest? Becau

Are you sure? If an AI would generate a huge Lean proof/program, wouldn't there be a way to hide such cheats in it? Like as in the underhanded C contest? Because if you give an AI a goal, and cheating at Lean would satisfy that goal, the AI will do it if it can figure it out.