Simplest theorem prover - General

Welcome to the Functional Programming Zulip Chat Archive. You can join the chat here.

Pedro Minicz

What is the simplest theorem prover/verifier/checker you know? This question is two fold: simplest implementation and simplest meta-theory.

Here are the ones I know:

Simplest implementation:

  • Victor Maia's implementation of Cedille Core: Based on the Aaron Stump's Calculus of Dependent Lambda Eliminations (CDLE). I believe this ties for the simplest implementation of a theorem prover with the next item on this list. Note that I mean simplest implementation, you gotta understand CDLE or it will seem like a quite weird extension of the Calculus of Constructions (CC).
  • Raph Levien's Metamath implementation in Python: ties for simplest implementation with the above.
  • Beckert and Posegga's leanTAP: its simple due to its size, but its written in quite compact Prolog which makes it harder to read. An interesting extension called alpha leanTAP exists, which is written in Scheme (using miniKanren, if I remember correctly). You can read more about it here.

Simplest theory:

  • Any implementation of Simply Typed Lambda Calculus. However, you can't prove many interesting things in it.
  • Metamath's formal grammar: Metamath is weird. I don't really understand its theoretical basis, it seems like it comes from the study of formal grammars. Mario Carneiro's paper Models for Metamath seems like a great resource, which unfortunately haven't had the time to read yet.
  • The Calculus of Constructions: many implementations of which exists, a few which come to mind are Morte and my own tiny (and hopefully correct) implementation.
  • The Calculus of Dependent Lambda Eliminations: its a very elegant (once you understand) extension of CC that derives induction.
Pedro Minicz

Hopefully, others can contribute for these lists. It is really hard to find truly small theorem provers (ones which you can hopefully read the entire source code in one sitting, from the ones above, only Morte doesn't fit this criteria). Also, if someone could please explain to me what exactly is going on with Metamath's meta-theory it would be much appreciated. :grinning_face_with_smiling_eyes:

Daniel Bramucci

I believe Formality is one of the simpler proof-languages implementation wise. But I haven't looked to closely at it.

An efficient proof language. Contribute to moonad/Formality development by creating an account on GitHub.
Pedro Minicz

Indeed. Formality is pretty cool. However, I don't believe its consistent. It has been a while since I've last checked it out, but back then, their goal had moved away from begin logically consistent to being nicer to program with.

Pedro Minicz

I would be great news if what they are doing with self types/insanely dependent types (I don't know what they call, but it is kind of mix of both of these concepts) actually happens to be consistent, i.e., not allow one to inhabit false.

James King

I've managed to get math-phobic and recreational people hooked on http://incredible.pm/

Albert ten Napel

A system based on "Gentle art of levitation" would be pretty simple to implement (except for cumulative universe which I haven't figured out yet). You start with dependent functions and pairs, add finite types (unit + bool for example) and then you add descriptions and fixpoints on them. Using the descriptions you can define inductive datatypes (or indexed types and even recursive-inductive and inductive-inductive types based on what descriptions you use) and define a induction principle for them. I think this gives you a lot of expressivity in a small package. I also I found elaboration easier to implement than CDLE or self-types.

Pedro Minicz

James King said:

I've managed to get math-phobic and recreational people hooked on http://incredible.pm/

Oh, very interesting, looks pretty cool. It remembered be of this interactive sequent calculus tutorial (spoiler: its pretty good).

Pedro Minicz

Albert ten Napel said:

A system based on "Gentle art of levitation" would be pretty simple to implement [...]

I remember stumbling upon this paper about a year ago. It looked a bit convoluted, but I was way less familiar with this stuff back then. Is there an implementation of it's type theory around somewhere?

Pedro Minicz

About (non-comulative) universes, Andrej Bauer implements them in his series How to Implement a Dependent Type Theory. I wonder how much more difficult comulative universes really are.

Pedro Minicz

I personally haven't implement them (actually, I have), but they look simpler than positivity checking, W-types, etc.

Minimal Type Theory with Universes and Pi Types. GitHub Gist: instantly share code, notes, and snippets.
Albert ten Napel

When I first looked at "Gentle art of levitation" I also found it convoluted, but after making some implementations of dependent type theories the implementation of datatypes using descriptions is actually much easier than native top-level datatype definitions. It's worth to give another look. Unfortunately I am unable to find any implementation of it, Epigram and Foveran (https://github.com/bobatkey/foveran) and Spire use them, but they are basically abandoned.

About universes, yes I've seen the implementation of Andrej Bauer but the difficulty I'm talking about is being able to lift definitions to different universes. You don't want to write the same definition multiple times just to use it in a higher level. This lifting operator is a bit tricky to implement from what I read, but I still need to spend more time on it.

A Dependently Typed Programming Language. Contribute to bobatkey/foveran development by creating an account on GitHub.
Albert ten Napel

And yeah, with descriptions you do not need to do any positivity checking, the description setup will ensure the datatypes are strictly-positive. The downside is that you are also more limited in which datatypes you can get.
I read that W-types are not good at all in an intensional setting, Conor McBride had a blog post on it that I am now unable to find.

Joey Eremondi

I'd add Cur to this list. It's basic idea is "provide a minimal type theory, and then use macros to build things on top of this". It also has the advantage of being built using Turnstile, so its implementation looks a lot like type rules: https://github.com/wilbowma/cur

A less devious proof assistant. Contribute to wilbowma/cur development by creating an account on GitHub.
Albert ten Napel

Ah that's very cool! Looks like Cur's core language is similar to the Calculus of Inductive Constructions. I will also link Dedukti/LambdaPi: https://github.com/Deducteam/lambdapi which is a type theory with rewrite rules. The core language is very simply, basically the Calculus of Constructions but I think the rewrite rules allow you to define more complicated theories inside of the language. I do wonder how consistency/canonicity is ensured though, if it is.

Proof assistant based on the λΠ-calculus modulo rewriting - Deducteam/lambdapi
Mario Carneiro

@Pedro Minicz I would also add to the list of simplest implementations the amazing turing machine written in an optimizing compiler called Not Quite Laconic (NQL) which was used to give a bound on the smallest undecidable busy beaver number. It was essentially a metamath kernel that enumerated proofs in ZFC looking for a contradiction

Mario Carneiro

it was something around a 1500 state TM whose termination could not be proved in ZFC (EDIT: here it is, 1919 states)

metamath proof enumerators and other things. Contribute to sorear/metamath-turing-machines development by creating an account on GitHub.
Mario Carneiro

Also HOL light definitely deserves to be in the running for simplest kernel; IIRC John Harrison has the implementation written on a T-shirt. I'm not sure if the actual kernel in the hol light distribution is as small as it could be, but here it is

The HOL Light theorem prover. Contribute to jrh13/hol-light development by creating an account on GitHub.