It also uses Prove2Me, which uses a graph like previous automated theorem provers. A fact that LLM hawks have categorically denied here before, with opposition naturally flagged.

Now they have it in writing.

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.