We have a significant case split here: A human mathematician writes a Lean proof: - Unlikely that the mathematician would cheat with Lean bugs or even know ho

We have a significant case split here: A human mathematician writes a Lean proof: - Unlikely that the mathematician would cheat with Lean bugs or even know how to find one. Trust increases. An AI writes a Lean proof: - AIs have been "ambitious" in their goals in the past and do know how to find Lean bugs and exploit them. Trust decreases.