Many of you here will have seen Randy Pollack's 1997 paper "How to believe a machine-checked proof".
Well, 29 years later, the first paragraph of the paper is very pertinent:
"Suppose I say “Here is a machine-checked proof of Fermat’s last theorem (FLT)”. How can you use my putative machine-checked proof as evidence for belief in FLT? I start from the position that you must have some personal experience of understanding to attain belief, and to have this experience you must engage your intuition and other mental processes which are impossible to formalise."
