This project is my personal attempt at making a theorem prover with an optimized interactive interface.

Motivation

We believe in the general principle: an ideal formal language is a coding scheme optimized for compression.

In particular, an ideal formal language for mathematics minimizes the cross-entropy¹ of human mathematics² under the language's uniform trajectory distribution³, subject to soundness and expressivity.

• Equivalently, it maximizes the probability that a monkey randomly hitting keys arrives at valuable theorems and proofs⁴, such that the proofs are always mathematically correct, and that nearly all mathematics can be generated this way.
• Equivalently, it is implicit in the exact objective of pre-training LLMs on formalized mathematics.

However, we do not have the compute to pre-train LLMs, so we take a more conventional, less compute-intensive path towards this goal: designing deterministic formal systems by hand.

• To lower the cross-entropy objective, the formal system should encode a wide range of proofs with fewer words (number of transitions) and smaller alphabets (number of branches at each transition) for each word.
• To satisfy the adequacy requirements, the formal system should accept only valid proofs, with soundness and completeness guarantees with respect to a common foundation of mathematics, e.g. some variant of dependent type theory.

Such deterministic systems are not expected to achieve similar levels of compression as entropy coding schemes induced by frontier LLMs, but encoding and decoding are cheaper, and they might act as better environments to start training new models on. For example, a randomly initialized model may find proofs easier, overcoming the initial reward sparsity.

This project does not aim to be a general-purpose programming language. Under the general principle, an ideal programming language minimizes the cross-entropy of useful programs under the language's uniform trajectory distribution. Despite the Curry-Howard correspondence, we consider that the distribution of "useful programs" to be very different from that of "human mathematics".

Design (TODO)

• My final year project report and slides. I am still working on the problems mentioned in the final chapter.

Examples (TODO; kernel only)

Example proof terms in the surface syntax:

• Some smalltt eval benchmarks: examples/tree_eval.zkt.
  • Type checking this term requires compiling with cargo build --features type_in_type.
• Linear-time environment lookup: examples/long_env_eval.zkt.
  • Should be acceptable if deeply nested lambdas/lets are uncommon, or can be uncurried using dependent tuples.
  • Linked frames with greedy extend did not seem to worth the complication. Even if lookup path lengths are reduced to nearly 1, the additional constant overhead seemed more significant, except on intentionally crafted benchmarks like this one.
• Constant-time dependent tuple lookup: examples/long_tuple_eval.zkt.
• Some basic first-order logic theorems: examples/first_order_logic.zt.

Footnotes

1. Equivalently, KL divergence can be used instead of cross-entropy. ↩

2. Assuming there is a single, stationary distribution. In practice, this can be approximated from large corpora of formalized mathematics. ↩

3. Defined as the distribution generated by uniformly sampling a word (transition) in the state-dependent alphabet (all valid transitions from a given state) repeatedly until reaching EOF. ↩

4. Defined as "more probable under the target distribution of human mathematics". ↩