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.
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 reformedWithoutEveryStrandsPremiseRead 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.
- Rationale — why machine-check testimony
- Scope and limits — what Lean does not settle
- Encoding arguments — how arguments become data
- Citations — bibliography conventions
- Roadmap — systematic and philosophical theology
- Contributing
lake exe cache get # fetch prebuilt Mathlib first — otherwise it builds from source
lake buildRequires 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.
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.
Two licences, split by what the file is:
- Code — Lean sources,
scripts/, build tooling: Apache License 2.0. - Documentation and data —
docs/, 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.