Knuckledragger is an attempt at creating a down to earth, highly automated interactive proof assistant in python. It is not attempting to be the most interesting, expressive, or flexible logic in the world. The goal is to support applications like software/hardware verification, calculus, equational reasoning, and numerical bounds.

python3 -m pip install git+https://github.com/philzook58/knuckledragger.git
python3 -m kdrag.solvers install # install extra solvers

Or to install locally

git clone https://github.com/philzook58/knuckledragger.git
cd knuckledragger
python3 -m pip install -e .
./install.sh # install extra solvers

• State of Knuckledragger, a Semi-Automated Python Proof Assistant
• Proving Sum n = n*(n-1)/2 and that 1/n tends to 0
• Peano Nats in Interactive SMT
• Experiments in the Irrationality of Sqrt 2 with SMT
• Knuckledragger Update: ATP for Python Interactive Theorem Proving
• Knuckledragger: Experimenting with a Python Proof Assistant

The design is based around the chaining of calls to z3. Python is a useful platform, but the core of the design can be ported to many languages.

• SBV - Haskell
• Yours here!

It is not desirable or within my capabilities to build a giant universe in which to live. The goal is to take a subtle blade and bolt together things that already exist.

Using widespread and commonly supported languages gives a huge leg up in terms of tooling and audience. Python is the modern lingua franca of computing. It has a first class interactive experience and extensive bindings to projects in other languages.

Core functionality comes from Z3. The Z3 python api is a de facto standard. The term and formula data structures of knuckledragger are literally z3 python terms and formula. To some degree, knuckledragger is a metalayer to guide smt through proofs it could perhaps do on its own, but it would get lost.

A hope is to be able to use easy access to Jupyter, copilot, ML ecosystems, sympy, cvxpy, numpy, scipy, egglog, Julia, Prolog, Maude, calcium, flint, Mathematica, and sage will make metaprogramming in this system very powerful. I maintain the option to just trust these results but hopefully they can be translated into arguments the kernel can understand.

The core logic is more or less multi-sorted first order logic aka SMT-LIB2.

Big features that ATPs do not often support are induction, definitions, and other axiom schema. Knuckledragger supports these.

Other theorem provers of interest: cvc5, Vampire, eprover, Twee, nanoCoP.

The de Bruijn criterion is going to be bent or broken in certain senses. Attention is paid to what is kernel and what is not. Proof objects are basically trees recording chains of lemmas discharged by Automated Theorem Prover (ATP) calls. Soundness will be attempted, accidental misuse will be made difficult but not impossible.

Isabelle and ACL2 are the strongest influences. If you want dependent type theory, you are at a level of investment and sophistication that it behooves you to be in another system. Should there be a strong automated DTT solver someday, I will reconsider.

I maintain the right to change my mind about anything.

TODO: A no-install WIP colab tutorial is available here