3
$\begingroup$

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

$\endgroup$
4
  • 3
    $\begingroup$ A nitpick: When you say ITPs 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", I am not sure you are using "kernel" in the right way. The kernel is the smallish part of the code that deals with only verifying, not QoL stuff. One wants to keep the kernel simple to avoid bugs. The only concerns are implementing the full logic correctly, and making it fast. The HOL kernels are quite tiny, especially HOL-Light. DTT kernels are larger. $\endgroup$
    – Jason Rute
    Commented Apr 26, 2023 at 11:41
  • 1
    $\begingroup$ Caveat: in spartan type theory you can prove whatever your heart desires because it thinks that 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$ Commented Apr 26, 2023 at 16:32
  • 3
    $\begingroup$ What is the purpose here? Educational? Note that small toy implementations won't get you very far if you try to formalize mathematics in a serious manner. $\endgroup$ Commented Apr 26, 2023 at 16:43
  • $\begingroup$ Thank you for the replies. I modify the question to describe better what I'm looking for. I was aware of the Type:Type problem with spartan, I assumed that is something not particularly difficult to fix if one wants to write their own kernel. $\endgroup$
    – Lewwwer
    Commented Apr 27, 2023 at 9:02

2 Answers 2

4
$\begingroup$

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.

$\endgroup$
1
  • 1
    $\begingroup$ Regarding the point on definitional equality, let me point out Weak Type Theory is Rather Strong by Boulier and Winterhalter, that shows that a theory entirely without definitional equality ("weak type theory") is conservative over extensional type theory (ie a theory with the most powerful definitional equality you can hope for). So indeed, definitional equality is really just a quality of life element, but does not change the provable theorems. $\endgroup$ Commented Apr 27, 2023 at 8:37
2
$\begingroup$

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.

$\endgroup$
7
  • 2
    $\begingroup$ Nice point about inductive definitions, etc. just being sugar for axioms. Indeed Metamath just implements all definitions as axioms if I understand correctly. $\endgroup$
    – Jason Rute
    Commented Apr 26, 2023 at 13:46
  • $\begingroup$ How do you handle definitional equality in your system? Is it checked automatically like in CiC? Or does one send every step explicitly to the kernel? $\endgroup$
    – Jason Rute
    Commented Apr 26, 2023 at 13:50
  • $\begingroup$ @JasonRute It is checked automatically using big-step reduction. I think it can be code-golfed even further using NbE, but that is quite confusing in the type system of Python. Weak type theory doesn't have (or rather, has a trivial) judgmental equality, and it is equi-translatable to intuitionistic type theory, you might be interested in that. $\endgroup$
    – Trebor
    Commented Apr 26, 2023 at 14:36
  • 2
    $\begingroup$ Now that we have CoC in Python someone should do ZFC in Excel. $\endgroup$ Commented Apr 26, 2023 at 16:38
  • 1
    $\begingroup$ @JasonRute I don't entirely agree that inductive definitions are just sugar for axioms. This isn't true in set theory nor in a pure MLTT kind of system $\endgroup$
    – Couchy
    Commented Apr 26, 2023 at 17:28

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.