Are there minimal typed proof verifiers that can deal with the majority of mathematics?

Question

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).

Answer 1

It is hard to give an answer without knowing your use case. But it is fairly easy to make a minimalist HOL theorem prover. The axioms of HOL are quite simple.

HOL-light is actually fairly minimalistic, especially if you ignore the tactics and pretty printing features. It uses the LCF framework, so all the inner workings are clearly exposed to the user. Also look at HOLPy. As for Metamath, it has an HOL system as well. Since it seems Metamath fits your definition of minimal, this might be what you are looking for.

As for dependent type theory, the logic is a bit trickier and spartan attempts, like cubicaltt, spartal type theory, and pie often have just one Type universe or the inconsistent Type : Type. (See Has anyone ever accidentally "proven" a false theorem with type-in-type?)

Edit: One reason that DTT is harder to implement than HOL is definitional equality. All the major DTT implementations automatically check if two terms are definitionally equal, which besides used in proofs, also is used for checking that theorem statements type check. You could implement a more bare bones version where the user has to go through every single step of the definitional equality calculation (see How does Metamath Zero handle CIC as in Lean or Coq?). Then it would be a lot more sparse, similar to HOL, but harder for the user.

But at the same time a number of people have written fully working external kernels for say the Lean theorem prover to check proof terms, including tc and trepplein, so it isn’t impossible to make your own DTT minimal checker with a full kernel.

Also again, I don’t know what you are looking for. You could use say Lean or Agda with term proofs only where you turn off all pretty printing. The tooling would be quite complicated, but your proofs would be quite bare bones.

Answer 2

Everything is almost trivial to implement if you strip it to bare bones. The Calculus of Constructions --- or more generally, pure type systems --- can be implemented in 100 lines of code, and if you write a simple parser on top of that, voilà! That's a proof assistant. You can now do tons of math, including to formalize an entire analysis book as is done in the 1970s. In fact, you can probably do all of math. No inductive types needed, because inductive types can simply be viewed as syntactic sugar that asserts a set of axioms and rewriting rules. You can do that yourself just as perfectly.

For comparison, here's a checker for first order logic: It checks that every step indeed follows from the previous ones from logical deductions. This one can also do tons of mathematics: Just dump in the axioms of ZFC, and you can proceed to formalize entire books of math with no problem.