Testimony

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 reformedWithoutEitherLexicalPremise

That last pair is the most useful thing the library does. Sola fide runs on two independent strands — Paul's ἔργα νόμου and Jesus' "your faith has saved you" at Luke 7:50 — so neither lexical premise carries it alone. An opponent must defeat both. The virgin-birth argument, by contrast, has only one strand, and defeating עַלְמָה defeats it outright.

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:

Code — Lean sources, scripts/, build tooling: Apache License 2.0.
Documentation and data — this site, the encoded premises, citations and generated prose: Creative Commons Attribution 4.0 International.

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