There was a recent announcement from Anthropic about using a team of agents to formalize Fermat's Last Theorem, and the generated artifact is over ten million lines of Lean code. At this point, one would question the utility of such an artifact: the issue is that humans still have to painstakingly check it, and make sure that there is no unsoundness bug. This raises the question of whether it is even theoretically possible to build a trusted-base against which all proofs are automatically trustworthy?
All proof assistant are just software, that a team of expert humans can verify, just like they can verify a human-crafted informal mathematical proof. Then, there is the entire software stack including the compiler, the standard library, and the OS kernel, and the entire hardware stack that also need to be verified. The difference between the mathematical proof and the hardware-software stack is that the mathematical proof is a frozen artifact, and a single verification is sufficient. On the other hand, hardware and software get updates, so a full verification of everything would get outdated long before it is completed. Even a minor update to anything still needs to be re-verified by humans.
Imagine that we freeze everything we currently have and verify it using a team of expert humans. Would it then be possible to use that as the trusted-base to mechanically verify all updates? The issue here is that our verification tools cannot express and check correctness of everything that a human can express and check correctness of. In fact, to build such a system, I conjecture that we'd essentially have to replicate a human in silicon (and verify that!).
The problem of building a mechanical trusted-base suffers from infinite regress. $\Box$