I would like to know if there are proof verifiers that can deal with the majority of mathematics (definitions, theorems, proofs with verification), while also having a minimal implementation. I am not looking for proof assistants with quality of life tools, syntax sugar, etc. Just the simplest verifiers.
EDIT: The motivation is that I wanted to learn more about proof verifiers, and I thought it would be good to write my own kernel and prove a few basic things in it, so I can convince myself that I can, in theory, do all the mathematics if I wanted to.
I am aware of metamath, as far as I know it is minimal and only uses substitution. But metamath is not based on type theory. Functions and relations are just sets, like everything else.
I know popular typed proof assistants can do a great deal of mathematics (isabelle, HOL/light, Coq, Lean), but from a quick glance, they have a pretty heavy kernel, dealing with all the quality of life help, to make them useful for the mathematicians rather than just a purely theoretical verifier.
EDIT: Thank you for pointing out that they don't all have big kernels. What I mean there, is that they still have huge implementations. It seems that these provers had large scale mathematics in mind when they were written. HOL-light has a tiny kernel, but to get to basics, let's say about integers, they define quite a lot of syntax sugar, tactics, then set theory, the reals and then they carve out the integers from them.
By googling, I've found spartan type theory but I am unsure if it is powerful enough to do a great deal of mathematics. In particular I can't see a way to create inductive types in the language, making it really difficult (or impossible) to argue about the naturals, for example.
EDIT: From the replies it seems that I should have included the motivation or at least a definition of "minimal" in my context. I hope these edits clear the question. In case there are no actual proof verifiers this simple, it would help a lot to have a tutorial explaining how to get from a kernel, (of the popular provers) to a point where I can define and prove basic things (like integers, addition and associativity).
Type : Type
. The purpose of spartan type theory is to have a very minimal implementation showing how one migth implement a kernel, i.e., that part of a proof assistant that just checks proofs. $\endgroup$