The Testimony mark: a turnstile with a cross inscribed at its intersection.

Testimony

A Lean 4 library for machine-checkable models of biblical arguments.

Testimony formalises Christian arguments from Scripture — that Jesus of Nazareth is the promised Messiah, that salvation is by grace through faith — with every textual, linguistic, historical, hermeneutical and theological premise made explicit, sourced, and contestable.

What this project is — and is not

Lean verifies that conclusions follow from encoded premises. It cannot, by itself, establish that an interpretation of an ancient Hebrew text is correct, that a historical event occurred, or that a theological premise is true.

So Testimony is not a "computer proves Christianity" system. It is a machine-checked testimony: the argument's structure laid bare, its assumptions enumerated, its verdict left to the reader. A sceptic can see exactly which premises are assumed; a believer can see precisely how the argument hangs together; a scholar can swap in a rival interpretation and watch the derivation diverge.

What it produces

Three kinds of result, all machine-checked:

An argument is valid. Given a named, cited premise package, the conclusion follows over every valuation.

theorem reformed_establishes : Establishes reformed

A rival package does not establish the conclusion. Not a failure to find a proof — a countermodel is named, and it is the rival's reading written down.

theorem tridentine_not_establishes : ¬ Establishes tridentine

A premise is, or is not, load-bearing. Remove it, retain everything else, and see whether the argument survives.

theorem worksOfLaw_not_load_bearing : Establishes reformedWithoutWorksOfLaw
theorem lexical_premises_jointly_load_bearing :
    ¬ Establishes reformedWithoutEveryStrandsPremise

That last pair is the most useful thing the library does. Sola fide runs on three independent strands — Paul's ἔργα νόμου, Jesus' "your faith has saved you" at Luke 7:50, and Peter's refusal of the law's yoke at Acts 15:10 — so no strand's disputed premise carries it alone. An opponent must defeat all three. The virgin-birth argument began with a single strand, where defeating עַלְמָה defeated it outright; it now runs on four, and no single interpretive hinge is load-bearing — only all four jointly.

Which argument has which shape is a fact about the encodings rather than a matter of emphasis, and the roadmap lists every result the library claims, generated from the Lean source by lake exe statusgen.

Each argument also has a page of its own — Sola scriptura is the longest — generated by lake exe argdoc from the Lean files themselves: the module docstrings as prose, every position and objection as typeset notation over one numbered legend of claims, and every result with the axioms it rests on. Nothing on those pages is written twice.

Getting started

lake exe cache get   # fetch prebuilt Mathlib — do this first
lake build

Requires elan. The toolchain is pinned to Lean v4.33.1 by the Foundation dependency.

License

Two licences, split by what the file is:

Scripture and the commentary literature are quoted for citation and criticism; those works remain under their own terms, recorded per entry in the bibliography.