In the previous blog posts (first, second, third), we wrote every theorem by hand. Recall how many steps it took to show that 1+1=2 with Peano’s axioms. This does not scale.
In this blog post, we will show how Budge-TP can write proofs for us.
Meta-programs
Budge-TP now supports meta-programs (really, just Python code) inside <?py ... ?> blocks. I vibecoded this feature with Claude, and it was super easy.
The semantics are simple: whatever the block prints is inserted into the file as Budge-TP code, and then checked like any other theorem. Basically, Python can’t prove anything by itself, it can only generate proofs, and Budge-TP still checks every step. This is the same idea as Edinburgh LCF: a small trusted checker, and a programming language on top of it.
A block also has access to env (all rules and theorems checked so far) and load(path) (to reuse other files), so we can now build libraries such as lib/logic.btp and lib/peano.btp.
Tired, wired, inspired
Let’s prove 0+n=n in three ways.
First, the way we did it in the previous posts, where each number needs its own theorem.
Next, we have Python generating these lines. Observe that the output is the same kind of theorems as before, i.e. Budge-TP doesn’t know (or care) that Python wrote them. However, we can only prove it for the numbers we ask for (up to tm4!).
Now, observe that the output is the same kind of theorems as before, i.e. Budge-TP doesn’t know (or care) that Python wrote them. However, we can only prove it for the numbers we ask for (up to tm4!).
This produces a single theorem, thZeroAdd : ⊢ALL(EQ(ADD(0,V(0)),V(0))), which really represents ∀n. 0+n=n.
Tactics
The functions used above (ind_hyp, chain, induction) come from lib/tactics.py, which is a small tactics language (really, just Python functions that print Budge-TP theorems). ind_hyp gives us the induction hypothesis, chain rewrites an equation step by step, and induction combines the base case and the step.
There are also tactics for natural deduction (assume, discharge, ex_i, ex_e, by_contra, …). For example, here’s how transitivity of divisibility (a|b and b|c implies a|c) starts in lib/divides.btp:
root = Ctx(reserved={a_, b_, c_})c1 = root.assume(dvd(a_, b_)) # assume a|bc2 = c1.assume(dvd(b_, c_)) # assume b|c# ... unpack both ∃s, rewrite c = b·y = (a·x)·y = a·(x·y), pack again ...h = root.close(c1.discharge(c2.discharge(...)))
With these, we can go a lot further than 1+1=2:
- Gauss’s sum formula
- Euclid’s theorem that there are infinitely many primes
- Euclid’s GCD algorithm verified with Hoare logic (and extracted to Python)
- A verified compiler from expressions to a stack machine
Conclusion
The checker is still about 300 lines of Python that only does substitution. The convenience comes from the meta-programs, and the correctness still comes from Budge-TP. That is, we got a new level of abstraction without having to trust it.
There is nothing really unique here. Rocq does the same thing with its tactics language (Ltac), and so do most proof assistants. But building it from scratch on top of a system that only does substitution gave me a better understanding of how much expressive power a meta-language adds, and how little of it needs to be trusted (assuming that the foundations it relies on (the checker and the axioms) can be trusted 🙂).
