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.
Lean verifies that conclusions follow from encoded premises. It cannot
establish that an interpretation of an ancient Hebrew text is correct, that a
historical event occurred, or that a theological premise is true. So this 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.
What it produces
theorem reformed_establishes : Establishes reformed
theorem worksOfLaw_not_load_bearing : Establishes reformedWithoutWorksOfLaw
theorem sozo_not_load_bearing : Establishes reformedWithoutSozo
theorem lexical_premises_jointly_load_bearing :
¬ Establishes reformedWithoutEveryStrandsPremise
Read together, those say something prose arguments rarely establish. 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 — and no disputed premise carries the argument by itself. Only a
disjunction does — Paul's two readings of Galatians 2:16, or Jesus' σῴζω, or
Peter's yoke — so an opponent must defeat a reading in each strand, not one
reading.
A corollary: the New Perspective on Paul, which rejects the traditional reading
of ἔργα νόμου while still affirming justification by faith, establishes the
conclusion too.
The virgin-birth argument used to make the contrast, and no longer does. It
began single-stranded, so defeating עַלְמָה in Isaiah 7:14 defeated it outright.
Three further strands — the protoevangelium of Genesis 3:15, Micah 5:2–3, and
Isaiah's own composition — changed its shape rather than its evidence:
almah_not_load_bearing now holds, while hinges_jointly_load_bearing records
that the four hinges still carry it jointly. The library states the structure
plainly whichever way it comes out, and the
roadmap lists every result it claims — generated from
the Lean source, not restated by hand.
Documentation
📖 Read the documentation
Getting started
lake exe cache get # fetch prebuilt Mathlib first — otherwise it builds from source
lake build # the library: the machinery for stating and checking arguments
cd arguments && lake build # the worked arguments, a package built on it
Requires elan. Lean v4.33.1, pinned by
the Foundation
dependency. Alternatively, open the repo in the devcontainer
(.devcontainer/) for elan, the pinned toolchain, tectonic, mdbook and
python3 preinstalled — the same image CI builds in.
Contributing
Two kinds of expertise make this work, and you only need one:
- Theology or biblical studies, no Lean required. Review whether an
encoding faithfully represents the argument it claims to. This is the
contribution the project most needs — a subtly wrong formalisation is worse
than none, and no proof assistant can catch it.
- Lean, no theology required. Types, proofs, tooling. The theological
content can be treated as opaque data.
See CONTRIBUTING.md.
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.
