Comment Comment by 3192987 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. parent 3192987 2 months ago
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.