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.