j-bob VS CORE

ACL2 is one prominent example of a theorem prover that uses a Lisp language (its manual is here). There's also an introductory book on using proof assistants called "The Little Prover," which uses a very simple Lisp-style theorem prover called "J-Bob" (with implementations in Scheme (the language that Guile, etc is an interpreter for) as well as ACL2). A major goal with J-Bob is that the prover itself is simple enough that its source code is easy to read, to make it easier to demonstrate to students (and anyone else interested in learning) how one kind of proof assistant could work.

Library of proofs Github repo

Back in March I started my fourth attempt at making a proof assistant, and to my surprise I actually succeeded. A proof assistant is a programming language for mathematical logic and proofs. I wanted to make my own simple proof assistant for set theory, which is a logic in which the objects are "sets," i.e. collections of other objects. Since the language's creation, I've been able to prove some basic facts about the natural numbers and construct addition and multiplication from scratch (using the ZFC axioms). I also made a website where you can look at all of the results I've proven in CORE. In the website you can recurse through results by clicking on the bold words in the code for the proofs. I have a repository for the language here. For the people who are interested, I will describe the language in more detail below.

Anyways, if anybody wants to take a look, the project is here. I'm not sharing the project with the expectation that people will actually use it, but I am certainly still interested in making the language more powerful. So if you have criticisms please keep this in mind!