[n4r9]

I asked a very similar question a couple of weeks ago here: https://news.ycombinator.com/item?id=44028051

The top answer helped me to understand.

> Presumably an AI would formalise the proof in a system such as Lean, then you only need to trust the kernel of that proof system.

[simiones]

I don't think trusting the Lean kernel is enough: you also need to trust that all of the Lean code is a valid translation of the informal proof. Given that the informal proof is already gigantic, and that there is no general mechanical way to verify if a formal statement corresponds 1:1 with an informal statement, it's far from trivial to trust that the Lean representation of the proof is the same thing as the original proof.

Now, if the proof works, presumably this problem goes away: Lean can show that based on this proof, the original statement holds. But if Lean says that this formal proof doesn't work, that doesn't tell you anything about the informal proof: the error may only be in the formalization.

[n4r9]

Agreed; translating to Lean/Coq is more likely to prove the positive rather than the negative. It may still be useful in pinpointing where incorrect proofs go wrong.