[digama0]

Luckily, this is a solvable problem. A theorem prover is software, so you can apply formal methods to it, and prove that the software performs its stated function. The CakeML project does this, and I'm working on a bootstrapping theorem prover (Metamath Zero) to do this in a few hundred lines of code. So it's not as hopeless as it seems. You just have to have a really efficient and simple checking algorithm and run it over a big computer generated proof of correctness, and it all scales very well. Then you can take that verified theorem prover and apply it to all the regular math we care about.

[YeGoblynQueenne]

But formal methods are also supported by theory where any theorems have proofs done by humans, which may contain mistakes. It's humans all the way down, see.