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

Testimony

Christian arguments from Scripture, written out premise by premise and checked by machine.

Testimony is two things.

  1. A guide for people reading an English Bible, written in language precise enough that a theologian can work with it. Each argument page starts from the passages, says in plain words what each side takes them to mean, and names who holds each view and where they wrote it.
  2. A code library for encoding arguments and checking them for consistency. Each position is a list of premises, every one with a source. Lean 4, a proof assistant, checks what follows from each list, what does not, and which positions can be held together.

If you came to read, start with an argument: Sola fide is the fullest. If you came to write code, start with Encoding arguments. Reading the logic explains the notation for anyone who has not met it.

What this project is, and is not

Lean checks that a conclusion follows from the premises written down. It cannot tell you that a reading of an ancient Hebrew text is right, that an event happened, or that a doctrine is true.

So Testimony is not a computer proving Christianity. It is an argument with nothing hidden. Every assumption is listed. Every rival reading is written out with the same care as the one it opposes. The judgement is left to the reader. A sceptic can see exactly what is assumed. A believer can see how the argument holds together. A scholar can swap in another reading and see what changes.

What it produces

Three kinds of result. Each is checked by machine.

A conclusion follows. Grant the premises of a named position, each with its source, and its conclusion follows.

theorem reformed_establishes : Establishes reformed

A conclusion does not follow. This is not a failure to find a proof. A consistent way of reading the texts is written down on which every premise holds and the conclusion does not. That reading is the rival position itself.

theorem tridentine_not_establishes : ¬ Establishes tridentine

An argument does, or does not, depend on a premise. Remove the premise, keep everything else, and see whether the conclusion still follows.

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 reaches "saved through faith" by four routes: Paul's "not by works of the law" (Galatians 2:16), Jesus' "your faith has saved you" (Luke 7:50), Peter's refusal of the law's yoke (Acts 15:10), and Jesus' "this is the work of God, that you believe" (John 6:29). Each route depends on one disputed reading. Remove any one and the others still reach the conclusion. Remove one from every route and it no longer follows. So an opponent has to answer all four.

The virgin-birth argument began with a single route, through the Hebrew word for "young woman" or "virgin" (עַלְמָה) in Isaiah 7:14, and defeating that one reading defeated the argument. It now has four routes, and depends on no single one of them.

A fourth kind of result weighs positions against each other and reports which survive. Those results often come out as ties, and the pages say so.

The roadmap lists every result the library claims, generated from the Lean source by lake exe statusgen, and a status page says how far the checks of meaning, ontology and fallacies reach in each argument. Each argument has a page of its own, generated by lake exe argdoc from the Lean files: the prose is the docstrings, the formulas are rendered from the encoding, and each result is shown 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.