[Theofrastus]

Things have moved on since then, as artificial intelligence has started being used in formalisation, [...]

With how AI works fundamentally, wouldn't you still need to verify the results generated by AI? Doesn't seem like an applicable field for it, at least in its current state.

[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.

[KK7NIL]

They use LLMs to help write formal proofs (in languages like Coq) that are then checked by traditional programs; they're not using AI as the checker.

https://youtu.be/e049IoFBnLA