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 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.

Rationale

The problem with arguing in prose

Christian arguments from Scripture are old, well developed, and almost always delivered as prose. A case that Jesus fulfils the messianic prophecies runs through dozens of texts, each requiring a reading, each reading resting on lexical, historical and hermeneutical assumptions that the argument rarely stops to enumerate.

This has three consequences, and they damage the argument's defenders more than its critics.

Premises hide. An argument that Micah 5:2 predicts the Messiah's birthplace assumes that Micah 5:2 is forward-looking prophecy rather than an oracle about a contemporary Judaean ruler. That assumption is doing real work. In prose it appears as a clause, or as nothing at all.

Disagreement diffuses. When two scholars disagree about sola fide, where exactly do they part company? Both accept that Paul wrote Romans 3:28. Both accept the text. Somewhere in a hundred pages of argument there is a step one grants and the other denies, and locating it is itself a research project.

Nobody can audit the whole. A cumulative case over twelve prophecies has a shape no reader holds in their head at once. Which conclusions depend on which premises? If one premise falls, what else falls with it? Prose cannot answer this, and neither can its author.

What formalisation changes

Encoding an argument in Lean does not make it true. It makes it inspectable, in four specific ways.

Premises become enumerable. Every atomic claim in a Testimony argument carries a citation, enforced by the type system: the function from atoms to their sources is total, so an uncited claim does not compile. The assumption manifest is then generated from the premises rather than maintained beside them, and cannot drift out of step with the argument it describes.

Validity becomes mechanical. Whether the conclusion follows is settled by truth table, checked by Lean's kernel. This is the least interesting guarantee the library offers, and it is worth having anyway: it means no disagreement about an argument is ever a disagreement about whether it is valid.

Disagreement becomes locatable. This is the real payoff. Encode the Reformed reading of justification, encode the New Perspective alongside it, and the library will tell you that the two packages differ in exactly one premise — whether Paul's ἔργα νόμου means works in general or Jewish covenant boundary markers — and that this premise is load-bearing: remove it and the Reformed argument collapses while everything else stays.

That result is not Protestant or Catholic. It is a description of the disagreement that both sides can accept, and it is the kind of thing prose almost never delivers.

Circularity becomes visible. A premise grounded only in Scripture is epistemically different from one grounded in scholarship, and the library types the difference. Source.isScriptureOnly computes it, and every argument reports its scripture-only atoms. An argument from Scripture that reads Scripture a particular way and cites only Scripture for that reading is assuming part of what it sets out to show. That is sometimes fine. It should never be invisible.

Why this is the stronger position, not the weaker one

It might look like a concession to publish every assumption an argument makes. It is the opposite.

An argument whose premises are all declared is harder to dismiss than one that claims more than it can deliver. The sceptic's usual move — you are assuming what you set out to prove — is answerable here by pointing at the manifest and asking which premise they reject, and on what grounds. The conversation moves from suspicion to a specific, arguable claim.

The library is also, deliberately, useful to people who reject its conclusions. A critical scholar who thinks Isaiah 7:14 is a near-term sign to Ahaz can encode that reading with the same machinery, and the library will confirm that the Christian conclusion does not follow from it. Both encodings live in the same repository. That is not neutrality for its own sake; it is what makes the Christian encodings worth taking seriously.

Prior art

Machine-checked theology is not new. The clearest precedent is Benzmüller and Woltzenlogel Paleo's formalisation of Gödel's ontological argument, which verified the proof in higher-order logic and found, in the process, that Gödel's axioms collapse modal distinctions — a result about a famous argument that a century of prose commentary had not established.

That is the pattern this project expects to repeat: formalisation rarely settles whether a conclusion is true, and frequently discovers something about the argument's structure that nobody had noticed.

See the bibliography for the citation.

Why a community

Two kinds of expertise are needed and almost nobody has both.

Formalising an argument requires knowing Lean. Judging whether a formalisation faithfully represents the argument it claims to represent requires knowing biblical studies, the history of interpretation, and the secondary literature. A subtly wrong encoding is worse than no encoding, because it launders a bad argument through a proof assistant and comes out looking rigorous.

So the review that matters most here is not a Lean review. It is a theologian or biblical scholar reading an encoding and saying that is not what the argument says. The project is set up to make that contribution possible without writing any Lean: see Contributing.

Scope and limits

This chapter states what the library does not do. It is here near the front, before the claims, on purpose.

What Lean settles

Exactly one thing: whether a conclusion follows from the premises as encoded. Lean's kernel checks that the truth-table computation is correct and that the bridge from it to the semantics is proved. Nothing else is verified by the machine.

What Lean does not settle

Whether the premises are true. That Micah 5:2 is a forward-looking prediction is an interpretive claim held by some traditions and denied by others. The library records who holds it, with what confidence, and on what authority. It does not adjudicate.

Whether the encoding is faithful. That a Lean formula represents the argument a commentary actually makes is a human judgement. No proof assistant can check it, and it is the most common way a formalisation goes wrong. This is why encodings need review by people who know the literature, and why a subtly wrong formalisation is worse than none.

Whether the atoms carve the argument correctly. Choosing eleven atomic claims for sola fide is already an interpretive act. A different carving might make a different premise load-bearing. The atoms are visible and arguable, and that is the best the method offers.

Whether the argument is the best one available. The library encodes particular arguments from particular sources. A better argument for the same conclusion may exist and simply not be encoded yet.

Circularity, specifically

An argument that Scripture predicts X, which reads Scripture as predicting X, and cites only Scripture for that reading, is assuming part of what it sets out to establish.

The library does not forbid this. Sometimes a text really is plain, and demanding external corroboration for every reading would be its own distortion. What the library does is make it computable: Source.isScriptureOnly is true exactly when a premise appeals to Scripture with no scholarly support, and ArgumentPackage.scriptureOnlyAtoms lists them.

In the Bethlehem argument, jesusBornInBethlehem is such a premise: the historicity of the Bethlehem birth is disputed in critical scholarship, and the argument assumes it on the authority of the texts whose reading is in question. That is stated in the module, and it is visible in the manifest.

The trust base

Results depend on Lean's kernel and on three axioms: propext, Classical.choice, and Quot.sound. Nothing else.

This is enforced rather than asserted. lake exe axiom-audit inspects the kernel environment — not the source text — and fails CI if any declaration depends on anything outside that allowlist. It catches sorry (which appears as sorryAx), native_decide (which adds Lean.ofReduceBool), and any hand-rolled axiom arriving through an import.

native_decide is prohibited outright. A project whose entire claim is that every assumption is declared cannot rest results on an undeclared one.

This gate has already earned its place. During development a decide proof failed silently and fell back to sorryAx; the axiom audit caught it, and the underlying API was removed.

What is deliberately out of scope for now

• Probabilistic and evidential reasoning. Cumulative-case arguments update on evidence; that is a different formal apparatus and will live in a separate namespace, never conflated with deduction.
• Corpus grounding. Passage values are references, not text. They do not yet resolve against real manuscript data.
• Modal logic. Needed for divine-attribute arguments; reachable from the chosen substrate but not yet used. See the roadmap.

Architecture

Testimony models arguments in layers. The guiding rule: formal validity and truth of premises are different things, and the library's job is to keep that boundary visible at all times.

Principles

1. Conditional analysis. Every theorem has the shape given premise package P, conclusion C follows. No premise is smuggled in.
2. Rival interpretations are first-class. Divergent conclusions are a feature. An argument module encoding a Christian reading without at least one rival package is incomplete.
3. Relation types are not collapsed. Quotation ≠ allusion ≠ typology ≠ prediction ≠ retrospective interpretation. Much of the messianic-prophecy debate is precisely about which of these a given link is.
4. Provenance everywhere. Enforced by the elaborator, not by review: see Citations.
5. Assumption manifests are generated, never maintained.
6. Canon is a parameter. Results are relative to a declared canon.

The layers

Two structural enforcements

The library's central rule — nothing is asserted bare — is enforced twice, at two levels, by making the bad state unrepresentable rather than by checking for it.

Source.primary is a single required Reference, not a possibly-empty list. An uncited Source cannot be written down. There is no free-text escape hatch, because an escape hatch would be used.

ArgumentPackage.cite is a total function from atoms to their metadata. An atomic proposition without a citation does not compile.

Neither of these requires a linter, a review checklist, or a proof obligation at the use site. They are consequences of the types.

Dependencies

The library depends on FormalizedFormalLogic/Foundation for its propositional syntax and semantics, and transitively on Mathlib, doc-gen4 and axiom-audit. Foundation pins Lean v4.33.1.

Foundation supplies the formula type, the Hilbert systems, the Boolean and Kripke semantics, and the metatheory; Testimony reimplements none of it. What Testimony adds is a decidability adapter, explained in Encoding arguments.

Encoding arguments

How entailment is settled

An argument is a list of premises and a conclusion, both formulas over cited atoms. Two questions get asked of it, and they are answered by different means.

Does the conclusion follow? Mathlib's tauto, a goal-directed classical tableau. It produces an ordinary proof term, so the trust base is unchanged, and its cost tracks the argument's structure rather than its atom count.

Does it fail to follow? Name a countermodel — a valuation satisfying every premise while falsifying the conclusion:

theorem not_entails_of_countermodel
    (w : Valuation α)
    (hsat : ∀ φ ∈ prems, Formula.Boolean.val w φ)
    (hfail : ¬ Formula.Boolean.val w concl) : ¬ Entails prems concl

Checking a named valuation is linear. Searching for one is not, which is why the library asks the author to supply it.

That turns out to be a feature rather than a chore. "A countermodel exists" tells a reader nothing; a named valuation is the rival's reading, written down. So countermodels here carry the rival's name — nppReading, tridentineReading, criticalReading — and a reader can inspect what the opposing position actually commits to.

There is no atom budget

An earlier version decided entailment by exhaustive truth table, which cost 2^n and forced a twelve-atom cap on every argument. Both are gone. An argument tracing a theme across the canon may use as many atoms as it needs.

What was rejected, and why

bv_decide, Lean's SAT-solver tactic, is fast and unusable here. It emits a per-theorem native axiom:

'bvtest' depends on axioms: [propext, Classical.choice, Quot.sound,
                             bvtest._native.bv_decide.ax_1_5]

That is an external solver's certificate entering the trust base. For a library whose claim is that every assumption is declared, it is not a trade worth making, and axiom-audit would reject it.

Foundation's proof calculi supply soundness and completeness metatheorems for the Tait calculus, but no executable decision procedure, so they cannot discharge a goal.

A hand-rolled pruning search was written and then deleted once tauto proved to handle the same goals with less machinery and no new proof obligations.

Rendering an argument as logic

lake exe argtex writes docs/latex/arguments.tex: every package set the way a logic paper would set it — a legend of numbered propositional variables with each one's claim, classification and source, then the premises and conclusion in ordinary notation.

lake exe argtex
cd docs/latex && tectonic arguments.tex    # or xelatex / lualatex

A Unicode engine is required: the claims contain Greek and Hebrew. Citations render as live \cite commands against the generated references.bib.

Atoms are numbered rather than named, which is the usual convention and the point of rendering at all. It separates an argument's shape from its content:

(12)  (P₄ ∧ P₅ ∧ P₁) → P₁₂
(13)  (P₈ ∧ P₂) → P₁₂
(14)  (P₉ ∧ P₁₀) → P₁₃
(15)  (P₁₂ ∧ P₃ ∧ P₆ ∧ P₇ ∧ P₁₃ ∧ P₁₁) → P₁₄
  ⊢   P₁₄

That is sola fide. Premises (12) and (13) both conclude P₁₂, one by way of P₁ (Paul's ἔργα νόμου) and one by way of P₂ (Jesus' σῴζω at Luke 7:50). The argument's redundancy — the reason neither lexical premise is load-bearing — is visible on the page before you read a word of the legend.

Writing an argument

An argument module has five parts.

1. An atom type, one constructor per atomic claim, each documented with what it asserts:

inductive Claim
  /-- Romans 3:28 teaches justification by faith apart from works of the law. -/
  | romans3_28
  /-- Paul's ἔργα νόμου denotes human works in general. **The disputed
  premise.** -/
  | worksOfLawMeansWorksGenerally
  ...
deriving DecidableEq, Repr

2. A total citation function. Because it is total, an uncited atom does not compile:

def cite : Claim → AtomMeta
  | .romans3_28 =>
    { label := "Romans 3:28 teaches justification by faith apart from works of the law"
    , kind := .textual
    , source := { primary := .scripture [{ ref := .verse ⟨.romans, 3, 28⟩ }]
                , supporting := [.work calvinInstitutes (.sectionRef "III.xi.19")]
                , tradition := .reformedProtestant
                , confidence := .wellSupported } }
  ...

3. Packages — rivals first. Writing the rival before proving anything keeps the encoding honest; it is much easier to build a strawman after you have a proof you like.

4. Theorems, tagged @[headline] and followed by #print axioms. To establish, unfold the package and call tauto:

@[headline]
theorem reformed_establishes : Establishes reformed := by
  intro w hw
  simp only [reformed, sharedPremises, paulineToFaithAlone, conjOf, p,
    List.mem_cons, List.not_mem_nil, or_false, forall_eq_or_imp, forall_eq,
    FFL.Propositional.Formula.Boolean.val] at hw ⊢
  tauto

To refute, name the rival's reading and check it:

def tridentineReading : Valuation Claim := fun a =>
  match a with
  | .salvationByGraceThroughFaithNotWorks => False
  | _ => True

@[headline]
theorem tridentine_not_establishes : ¬ Establishes tridentine := by
  refine not_entails_of_countermodel tridentineReading ?_ ?_ <;>
    simp [tridentine, conjOf, p, notP,
      FFL.Propositional.Formula.Boolean.val, tridentineReading]

Qualify FFL.Propositional.Formula.Boolean.val in full: Formula is also an abbreviation in Testimony.Logic, and the unqualified name resolves there.

5. The load-bearing results, where there is a disputed premise. State the reduced package explicitly:

def reformedWithoutWorksOfLaw : ArgumentPackage Claim :=
  { reformed with
    name := "Reformed, minus the Pauline lexical premise"
    premises := [ ... everything except the disputed premise ... ] }

Then ask whether the argument survives. Where an argument has two independent strands, as sola fide does, neither disputed premise is load-bearing alone — only their disjunction is, and that is the more interesting result.

Manifests

Generated from the premises, never maintained beside them:

def ArgumentPackage.manifest           : List AtomMeta
def ArgumentPackage.scriptureOnlyAtoms : List AtomMeta

manifest is every atom the premises rest on, deduplicated and mapped through cite. scriptureOnlyAtoms filters it to those appealing to Scripture with no scholarly support — the circularity surface described in Scope and limits.

Citations

Every claim in this library carries a citation, and the citation is a typed value rather than a string. The point is that a reader can check it.

The binding rule

No bibliographic identifier is ever written from memory.

Verify every ISBN, DOI, edition statement, publisher and page range against a public catalogue before committing it. If a field cannot be verified, leave it none.

An entry with no identifier renders in the bibliography as (no public identifier). That is the rule working, not failing: five of the fourteen seed entries carry no identifier, because none could be tied to a specific printing. A plausible-looking wrong ISBN is far worse than an honest gap, because it survives review — it looks exactly like a right one.

Useful catalogues: Open Library (/search.json, /isbn/{isbn}.json) and Crossref for DOIs.

Entry types

Two distinctions that are easy to get wrong:

criticalEdition versus book. A critical edition has editors rather than authors, and is cited by siglum (NA28) and apparatus location rather than by page. If you would cite it as "NA28 at Matt 1:23", it is a criticalEdition.

ancientWork versus its modern edition. Scholarly practice cites Josephus, Ant. 18.63, in a named Loeb volume. Encode the ancient work with editionUsed pointing at the modern edition's key; the registry checks the reference resolves.

Adding an entry

1. Verify against a public catalogue. Leave unverifiable fields none.

2. Add a tagged definition to Testimony/Bib/Works.lean. The tag is what puts it in the registry; an untagged entry is invisible to bibgen and linter rule L4 rejects it.

   /-- Why this work is cited here. -/
   @[bib_entry] def mooRomans : BibEntry := .book
     { core :=
         { key := "moo-romans-2018"
         , contributors := { authors := [.person "Douglas J." "Moo"] }
         , title := "The Letter to the Romans"
         , year := some { value := 2018 }
         , identifiers := [.isbn "9780802871268"] }
     , publisher := "Wm. B. Eerdmans"
     , place := some "Grand Rapids"
     , edition := some "2nd edition"
     , series := some "New International Commentary on the New Testament" }
   

   Citation keys are family-shorttitle-year, lowercase, hyphen-separated. Rule L7 and a compile-time #guard both check the format.

3. Cite it from a Source, with a pinpoint:

   source :=
     { primary := .work mooRomans (.adLoc ⟨.romans, 3, 28⟩)
     , tradition := .reformedProtestant
     , confidence := .wellSupported }
   

4. Regenerate and commit both generated files:

   lake exe bibgen
   git add references.bib docs/src/bibliography.md
   

   CI runs lake exe bibgen --check and fails if they are stale.

Pinpoints

Locus says where in a work:

(sectionRef rather than section, because section is a Lean keyword.)

Scripture is not a bibliography entry

Scripture citations use a separate Reference constructor over typed passages:

primary := .scripture
  [ { ref := .verse ⟨.matthew, 2, 1⟩ }
  , { ref := .range ⟨.luke, 2, 4, 2, 7⟩ } ]

This is not a stylistic choice. It makes citations traversable — "what cites Isaiah 7:14?" is answerable — and it makes Source.isScriptureOnly computable, which is how the library surfaces circularity. See Scope and limits.

Generated outputs

lake exe bibgen writes two files from the Lean source, both committed:

• references.bib — biblatex-flavoured, for Zotero, pandoc and LaTeX
• docs/src/bibliography.md — the bibliography chapter of this book

Neither is edited by hand. lake exe bibgen --check verifies they match.

Entry types map onto BibTeX as follows. If you add a variant to BibEntry, extend Testimony/Bib/Render.lean and add a golden test for it.

Style guide

Conventions, and the command that enforces each one. A rule that lives only in prose is a rule that gets broken by someone in a hurry, human or agent, and nobody notices for months.

The four tiers

Run them in this order. Each catches what the previous one cannot.

Plus lake exe bibgen --check and lake exe argtex --check for generated-file drift.

lake build passing is not "it builds". Three further gates exist, and tier 3 in particular catches things nothing else will — a decide proof that silently fails and falls back to sorryAx produces a successful build.

Naming

• lowerCamelCase for definitions, snake_case for theorem names, after mathlib convention.
• Scripture-reference defs are the one exception: micah5_2, isaiah7_14, matthew1_23. The underscores are meaningful — they are chapter and verse. These carry @[nolint defsWithUnderscore], so the exception is declared rather than silent.
• Atom constructors read as passage + claim: romans3_28, worksOfLawMeansWorksGenerally, timothy3_16GodBreathed.
• Citation keys are family-shorttitle-year: france-matthew-2007, na28-2012.

Docstrings

Required on every declaration — enforced by linter.missingDocs at build time and docBlame/docBlameThm in lake lint. docBlameThm is disabled by default in Batteries and deliberately enabled here.

This is not decoration. A docstring in this library states what a premise asserts and who holds it, so an undocumented premise is very nearly an uncited one, and a theorem asserting a theological result must say what it claims.

• Atoms and premises: what is asserted, and which tradition asserts it.
• Packages: which position it encodes.
• Headline theorems: what it does and does not establish.
• Module docstrings: the layer, the purpose, and — for argument modules — a prose statement of the dispute. BornOfAVirgin.lean is the model.

The one exception is Book, where missingDocs is disabled for that declaration alone with the reason recorded inline: a constructor named genesis is documented by its name.

Encoding

• Rivals are not optional. An argument module encoding a Christian reading without at least one rival package is incomplete, not merely unpolished. Write the rival before proving anything. Rule L5 enforces this.
• There is no atom budget. Entailment is settled by tauto and refuted by named countermodels, neither of which enumerates valuations.
• State reduced packages explicitly; do not filter premises out of an existing package.
• Name your countermodels after the position they encode. A countermodel is the rival's reading written down, and a reader should be able to see what it commits to.
• Never native_decide, never sorry. This also rules out bv_decide, which adds a per-theorem native axiom.

Layout

Line width at most 100 columns; no trailing whitespace.

Domain linter rules

scripts/testimony_lint.py, tier 4. Every rule has a test that must trip it and a test that must not — a linter that silently stops firing is worse than no linter.

Run its own tests with python3 scripts/test_testimony_lint.py.

@[headline]

Marks a result the library actually claims, as against a supporting lemma. It makes "what does this library assert?" a greppable question, and rule L6 requires every headline result to display its trust base with #print axioms — documentation in the source for a reader of the argument, where the axiom audit is the gate for CI.

Bibliography

Every work cited anywhere in the library, generated from the Lean source. Machine-readable BibTeX is at references.bib.

25 entries, of which 6 carry no stable public identifier.

• na28-2012 — Barbara Aland, Kurt Aland, Institut für neutestamentliche Textforschung (ed.). Novum Testamentum Graece. Stuttgart: Deutsche Bibelgesellschaft. 28th revised edition. Siglum NA28. 2012. ISBN 9781619700321. ISBN is the Hendrickson / German Bible Society printing.
• benzmuller-godel-2014 — Christoph Benzmüller, Bruno Woltzenlogel Paleo. Automating Gödel's Ontological Proof of God's Existence with Higher-order Automated Theorem Provers. In ECAI 2014. IOS Press. Frontiers in Artificial Intelligence and Applications 263. 2014. DOI 10.3233/978-1-61499-419-0-93.
• berry-virgin-birth-2003 — Everett Berry. Virgin, Virgin Birth. In Holman Illustrated Bible Dictionary, ed. Chad Brand, Charles Draper, Archie England, Trent C. Butler, 1653–1654. Nashville, TN: Holman Bible Publishers. 2003. ISBN 9780805428360. ISBN is the containing volume's.
• brown-birth-messiah-1993 — Raymond E. Brown. The Birth of the Messiah: A Commentary on the Infancy Narratives in the Gospels of Matthew and Luke. New York: Doubleday. new updated edition. Anchor Bible Reference Library. 1993. ISBN 9780385472029.
• calvin-institutes-1960 — John Calvin. Institutes of the Christian Religion. Translated by Ford Lewis Battles. Philadelphia: Westminster Press. Library of Christian Classics. 2 vols. 1960. ISBN 9780664220211. Original Latin 1559.
• chilton-isaiah-targum-1987 — Bruce D. Chilton. The Isaiah Targum: Introduction, Translation, Apparatus and Notes. Wilmington, DE: Michael Glazier. The Aramaic Bible 11. 1987. ISBN 9780894534805.
• dunn-new-perspective-2005 — James D. G. Dunn. The New Perspective on Paul. Tübingen: Mohr Siebeck. Wissenschaftliche Untersuchungen zum Neuen Testament. 2005. ISBN 9783161486777.
• etcbc-bhsa — Eep Talstra Centre for Bible and Computer. Biblia Hebraica Stuttgartensia (Amstelodamensis). ETCBC, Vrije Universiteit Amsterdam. https://github.com/ETCBC/bhsa.
• bhs-1997 — Karl Elliger, Wilhelm Rudolph (ed.). Biblia Hebraica Stuttgartensia. Stuttgart: Deutsche Bibelgesellschaft. 5th edition. Siglum BHS. 1997. (no public identifier)
• france-matthew-2007 — R. T. France. The Gospel of Matthew. Grand Rapids: Wm. B. Eerdmans. New International Commentary on the New Testament. 2007. ISBN 9780802825018.
• johnson-james-1995 — Luke Timothy Johnson. The Letter of James: A New Translation with Introduction and Commentary. New York: Doubleday. Anchor Bible. 1995. ISBN 9780385413602.
• keil-delitzsch-minor-prophets-1949 — Carl Friedrich Keil, Franz Delitzsch. Biblical Commentary on the Old Testament: The Twelve Minor Prophets. Translated by James Martin. Grand Rapids: Wm. B. Eerdmans. 1949. (no public identifier) Reprint of the T. & T. Clark translation; original German 1866–68.
• marshall-luke-1978 — I. Howard Marshall. The Gospel of Luke: A Commentary on the Greek Text. Grand Rapids: Wm. B. Eerdmans. New International Greek Testament Commentary. 1978. ISBN 9780802835123.
• miravalle-introduction-mary-2020 — Mark I. Miravalle. Introduction to Mary: The Heart of Marian Doctrine and Devotion. Goleta, CA: Queenship Publishing. 2020. ISBN 9781882972067. ISBN is shared with the 1993 and 1997 Queenship printings; pagination cited is the 2020 printing's.
• miravalle-meet-mary-2007 — Mark I. Miravalle. Meet Mary: Getting to Know the Mother of God. Manchester, NH: Sophia Institute Press. 2007. ISBN 9781933184326.
• moo-james-2000 — Douglas J. Moo. The Letter of James. Leicester: Apollos. Pillar New Testament Commentary. 2000. ISBN 9780851119779.
• motyer-isaiah-1993 — J. Alec Motyer. The Prophecy of Isaiah: An Introduction and Commentary. InterVarsity Press. 1993. (no public identifier)
• openscriptures-oshb — Open Scriptures. Open Scriptures Hebrew Bible. CC BY 4.0. https://github.com/openscriptures/morphhb.
• postell-isaiah-messianic-2025 — Seth D. Postell. Is Isaiah 7:14 Messianic?. Journal of the Evangelical Theological Society 68.3: 465–493. 2025. https://etsjets.org/wp-content/uploads/JETS_68.3_465_Postell.pdf.
• rico-gentry-infant-king-2020 — Christophe Rico, Peter J. Gentry. The Mother of the Infant King, Isaiah 7:14: 'almâ and parthenos in the World of the Bible — A Linguistic Perspective. Eugene, OR: Wipf & Stock. 2020. (no public identifier) Three 2020 printings catalogued (ISBNs 9781498230162, 9781498230179, 9781498230186); none could be tied to a printing.
• tanner-decrees-1990 — Norman P. Tanner (ed.). Decrees of the Ecumenical Councils. Washington, DC: Georgetown University Press. 2 vols. 1990. ISBN 9780878404902.
• ubs5-2014 — United Bible Societies (ed.). The Greek New Testament. Stuttgart: Deutsche Bibelgesellschaft. 5th revised edition. Siglum UBS5. 2014. (no public identifier)
• wegner-virgin-births-2011 — Paul D. Wegner. How Many Virgin Births Are in the Bible? (Isaiah 7:14): A Prophetic Pattern Approach. Journal of the Evangelical Theological Society 54.3: 467–484. 2011. https://etsjets.org/wp-content/uploads/2012/01/files_JETS-PDFs_54_54-3_JETS_54-3_467-484_Wegner.pdf.
• westminster-confession-1647 — Westminster Assembly. The Westminster Confession of Faith. Westminster Assembly. 1647. (no public identifier) Cited by chapter and section; no critical edition catalogued.
• wright-what-paul-said-1997 — N. T. Wright. What Saint Paul Really Said: Was Paul of Tarsus the Real Founder of Christianity?. Grand Rapids: Wm. B. Eerdmans. 1997. ISBN 9780802844453.

Roadmap

Where the library is

Four arguments are worked end to end, each with at least one rival package:

Two findings emerged that were not designed for.

Redundancy defeats a lexical dispute. Sola fide runs on two independent strands — Paul's ἔργα νόμου and Jesus' σέσωκέν σε at Luke 7:50 — and neither lexical premise carries the argument alone. Only their disjunction does. An opponent must defeat both readings, not either.

The virgin-birth argument was the weaker one, and stopped being so. It began single-stranded, and almah_is_load_bearing recorded that defeating עַלְמָה defeated it outright. Adding the protoevangelium (Genesis 3:15), Michean (Micah 5:2–3) and compositional (Isaiah 2–12) strands changed the structure, not the Isaianic evidence: almah_not_load_bearing now holds, while almah_is_load_bearing_alone preserves the original finding about the Isaianic strand taken by itself.

The same module carries a referential reply that answers the lexical dispute without entering it — עַלְמָה need not mean "virgin" for Mary to be one — and compatibility_does_not_establish_criterion records its price: the reply is purely defensive. The contrast between these arguments is a structural fact about them, not a matter of taste, and the library states it in a form either side can check.

A corollary worth noting: because the New Perspective rejects the traditional reading of Paul's phrase while still affirming justification by faith, it establishes the conclusion too. Winning the ἔργα νόμου argument is not a defeat of sola fide.

Near term

More messianic prophecies (#1, #2). The canonical dozen — Isaiah 53, Psalm 22, Zechariah 9:9, Daniel 9, Psalm 110 — each with competing packages. Then the first aggregate result: a MessiahDefinition with several criteria and a MeetsDefinition theorem, which will expose how sensitive a cumulative case is to its weakest link.

The remaining solas (#3). Sola gratia, solus Christus, soli Deo gloria, and completing sola scriptura past its seed.

Corpus grounding (#4). Importers so Passage values resolve against real text data (BHSA, OSHB, STEPBible). At that point linguistic premises can cite actual morphological annotation rather than a commentary's report of it — which matters most for exactly the lexical premises that keep turning out to be load-bearing.

Old Testament Book completion (#5). The New Testament is complete; the Old is partial. A good first contribution.

Systematic theology

The natural extension. Doctrine is already structured the way this library wants: confessional standards state positions in numbered articles, and the relations between doctrinal loci are exactly the dependency structure the manifest machinery tracks.

• Confessional standards as versioned, citable axiom sets (#6) — the Nicene Creed, the Chalcedonian Definition, the Westminster Confession, the Catechism of the Catholic Church. Each becomes an ArgumentPackage whose atoms cite specific articles.
• Cross-locus consistency checking. Do a tradition's commitments on Christology, the atonement and justification cohere? This is a question about a set of formulas, and it is decidable for the propositional fragment.
• Dependency tracing. Which doctrines rest on which exegetical premises? If a reading of Romans 5 is abandoned, what else moves? Prose systematic theology cannot answer this; a generated manifest can.

The divinity of Christ is the obvious target and the hardest: it is a cumulative argument drawing on the Johannine prologue, the ego eimi sayings, worship texts, and the Chalcedonian settlement's reading of all of them. It should be attempted only once the aggregate machinery has been tested on the messianic prophecies, where the premises are simpler.

Philosophical theology

This is why the substrate choice matters. Foundation supplies modal logic and Kripke semantics, so the arguments that need □ and ◇ are reachable without changing foundations.

• Divine attributes and their alleged incompatibilities. The omnipotence paradoxes, and the foreknowledge/freedom problem — where the formal question is whether a set of attribute definitions is jointly satisfiable, which is precisely what a model-theoretic treatment settles.
• The classical arguments. Cosmological, ontological, moral. The ontological argument is the best-charted territory: Benzmüller and Woltzenlogel Paleo's machine-verified formalisation of Gödel's proof both demonstrates feasibility and illustrates the payoff, having discovered that Gödel's axioms collapse modal distinctions — a structural fact a century of prose commentary had missed.
• Theodicy structures. The logical problem of evil is a consistency claim about a premise set, which is the shape of problem this machinery handles best.

Infrastructure

• An assumption-manifest browser (#7) on the docs site: every theorem, every premise it rests on, every citation, cross-linked.
• Literate sources (#9). Prose and Lean interleaved in the .lean files, in the coqdoc tradition, rendering to PDF. This is currently blocked on tooling rather than on effort. Alectryon plus LeanInk was the path, and LeanInk is archived — last pushed in July 2024, pinned to Lean v4.6.0-rc1. Verso is actively developed and has a TeX backend, but it is HTML-first and inverts the model: documents embed Lean rather than Lean files carrying prose. Until one of those changes, lake exe argtex covers the part that matters most — the arguments themselves, typeset as logic.
• Probabilistic and evidential reasoning (#10), in a separate namespace, never conflated with deduction. Cumulative-case apologetics is Bayesian in structure, and pretending otherwise would misrepresent it.
• API documentation (#8). doc-gen4 arrives transitively via Foundation and the Testimony:docs facet works, but lake build Testimony:docs generates documentation for the entire Mathlib closure, which is far too slow to run in CI. Publishing API docs needs either a way to scope generation to this library's own modules, or a separately cached job. It is deliberately absent from the docs workflow until then.

Development environment

• A devcontainer (#11), so that the toolchain is consistent and not only the worktree layout. Contributors should not have to install elan and match Lean v4.33.1 by hand.
• Enforcing the worktree rule (#12). Every other hard rule in CLAUDE.md is enforced by a command; this one is documented and unchecked.

How deferred work is tracked

Everything above is a GitHub issue; the roadmap label marks the items seeded from this page, and infra the build and developer-environment ones. This page says why a thing is worth doing; the issue is where its state lives. When the two disagree, the issue is current.

What will not change

The conditional form of every result, the requirement that rivals be encoded with equal care, and the prohibition on undeclared axioms. These are what make the rest worth reading.

Contributing

Two kinds of expertise make this project work, and you only need one of them.

If you know theology or biblical studies (no Lean required)

This is the contribution the project most needs, and it does not require writing any code.

• Review encodings. Does the formal statement faithfully represent the argument it claims to represent? Are the atoms carved correctly? Is a premise missing? A subtly wrong formalisation is worse than none, because it launders a bad argument through a proof assistant and comes out looking rigorous. No proof assistant can check this; only you can.
• Propose rival packages. What does a given tradition actually assume? The library is only as good as its rivals, and a strawman rival is worse than useless.
• Source citations. Commentaries, journal articles, critical editions — with identifiers that can be verified. See Citations.
• File issues in plain English. Maintainers will pair with you on the Lean.

If you know Lean (no theology required)

• Type design, proofs, tactics. The theological content can be treated as opaque data; the engineering problems stand on their own.
• Tooling: bibgen, the domain linter, doc generation, CI.
• The logic layer: the decidability adapter and its bridge theorems are the most interesting code in the repository.

Ground rules

1. Honesty over advocacy. The library models arguments; it does not campaign. Rival interpretations are encoded with the same care as the Christian ones.
2. Every premise carries a source. Uncited premises do not merge — and, as of the citation layer, do not compile.
3. No invented identifiers. Verify against a public catalogue, or leave the field none.
4. No collapsing relation types. If a passage is disputed between "prediction" and "typology", encode both, attributed.
5. Respectful discourse. People of all faiths and none are welcome here. Debate the encoding, not the person.

Workflow

Work happens in a git worktree, one per branch, never in the primary checkout. Worktrees keep an in-progress encoding from colliding with a review of someone else's, and they matter more here than in most repositories because a Lean build is slow enough that switching branches in place means rebuilding.

scripts/new-worktree.sh my-branch         # worktree + Mathlib cache, ready to build
cd ../testimony-worktrees/my-branch

.lake/ is gitignored, so a fresh worktree does not inherit it from the checkout you branched from. The script runs lake exe cache get for you; skipping it means the first build compiles Mathlib from source, which takes hours rather than minutes.

The worktree script fixes the repository layout; it does not fix the toolchain. For that, open a worktree in the devcontainer (.devcontainer/) instead of installing elan, tectonic and mdbook by hand — it is the same image CI builds in, so a discrepancy between "works for me" and "works in CI" means the image is wrong, not your machine.

lake exe cache get                        # what the script runs for you
lake build                                # tier 1
lake lint                                 # tier 2
lake exe axiom-audit                      # tier 3
python3 scripts/testimony_lint.py         # tier 4
lake exe bibgen --check                   # generated files current

All of these run in CI. Small pull requests, one concern each. Discuss significant design changes in an issue first.

See the style guide for conventions, and Encoding arguments for how to write a new one.