Proof assitants have nothing to do with neural nets or optimisation. They are entirely determinitsic and return an absolute "true" or "false" result, not an approximation.

https://en.wikipedia.org/wiki/Proof_assistant

This is Good Old-Fashioned AI, through and through.

It's not really like that. NN's are only used when searching for new proofs or steps which can be used to fill in details, the verification of a finished proof is done by a classical program by a series of substitutions which are very straightforward and spelled out in detail.

Here is an example.

https://arxiv.org/pdf/1608.02644.pdf

You seem to think "AI" means machine learning. In this case it does not. Theorem prover systems don't use neural nets.

That's not the suggestion. Proof verification is easy (for a proof written in a formal system). Proof search is hard. Many (most/all?) proof assistants heavily use heuristics to guide the proof search. Machine learning on a database of proofs could lead to superior heuristics and make proving stuff in the formal systems easier.

Proving stuff in these systems is still harder than natural language proofs, so making them easier could increase adoption, which would make mathematicians' results more robust/rigorous.

Note that this is editorial license on the part of the writer; Buzzard is proposing the use of interactive theorem provers, which only use a small amount of 80's style AI (backtracking search and higher order matching). No one in ITP is seriously using modern neural net based AI in real theorem provers yet, although there are several research teams working on it.