In an unrelated thread Sam Nead intrigued me by mentioning a formalized proof of the Jordan curve theorem. I then found that there are at least two, made on two different systems. This is quite an achievement, but is it of any use for a mathematician like me? (No this is not what I am asking, the actual question is at the end.)
I'd like to trust the theorems I use. To this end, I can read a proof myself (the preferred way, but sometimes hard to do) or believe experts (a slippery road). If I knew little about topology but occasionally needed the Jordan theorem, a machine-verified proof could give me a better option (and even if I am willing to trust experts, I could ensure that there are no hidden assumptions obvious to experts but unknown to me).
But how to make sure that a machine verified the proof correctly? The verifying program is too complex to be trusted. A solution is of course that this smart program generates a long, unreadable proof that can be verified by a dumb program (so dumb that an amateur programmer could write or check it). I mean a program that performs only primitive syntax operations like "plug assertions 15 and 28 into scheme 9". This "dumb" part should be independent of the "smart" part.
Given such a system, I could check axioms, definitions and the statement of the theorem, feed the dumb program (whose operation I can comprehend) with these formulations and the long proof, and see if it succeeds. That would convince me that the proof is indeed verified.
However I found no traces of this "dumb" part of the system. And I understand that designing one may be hard. Because the language used by the system should be both human-friendly (so that a human can verify that the definitions are correct) and computer-friendly (so that a dumb program can parse it). And the definitions should be chosen carefully - I don't want to dig through a particular construction of the reals from rationals to make sure that this is indeed the reals that I know.
Sorry for this philosophy, here is the question at last. Is there such a "dumb" system around? If yes, do formalization projects use it? If not, do they recognize the need and put the effort into developing it? Or do they have other means to make their systems trustable?