ICM2022 でSpecial Plenary Lecturesを
行ったKevin Buzzard.

> it is clear that it is not accepted by the
mathematical community in general.

・What is the point of computers?
A question for pure mathematicians

4.3. Checking proofs.

Some computer scientists have argued that mathematicians are sloppy, and our literature has errors in, and that this problem can be
solved with computer proof assistants. Such an argument might initially look plau
sible, and I myself was a proponent of it a few years ago, but it does not stand up
to much scrutiny. Firstly, the experts in our community know which results can
be relied upon. Secondly, many errors are not serious and can be fixed.

Thirdly,
the more serious instances of this problem cannot be solved with computer proof
assistants right now anyway. A great example is Mochizuki’s claimed proof of the ABC conjecture [Moc21]. This proof has now been published in a serious research
journal, however it is clear that it is not accepted by the mathematical community
in general.