The formal logic of law, in Lean 4.
Law is a formal system: a body of enacted texts whose consequences follow from the texts themselves. Lawlib holds law the way Mathlib holds mathematics — as exact definitions and machine-checked theorems. Anything that is law belongs here — statutes, regulations, agency tables, court-made rules, any jurisdiction — as long as each piece declares exactly what it depends on.
What's in it today: United States federal tax and benefit law — about 1,000 parameters (every rate, threshold, and bracket table, as exact fractions with the date each value took effect) and ~700 formulas spanning the income tax, the EITC, the Child Tax Credit, SNAP, SSI, the ACA premium credit, Medicare/Medicaid eligibility, and payroll taxation. Current sources: mechanically imported from PolicyEngine US (the largest living model of US tax-benefit law), plus an independent hand-encoding of 26 U.S.C. §32 in Catala. Those are where we started, not where it ends. Scope and the taxonomy of legal sources: docs/scope.md; the design doctrine (why law is provable territory and data is not welcome here): docs/categories.md. State and local programs are parked in parked/states/ pending their own pass.
The import rule is strict — translate exactly or not at all.
A formula the translator cannot express faithfully becomes a declared
input, and the refusal is logged with its reason in
rejection_report.md. And the translation is
checked from outside: every night, thousands of randomized households
are computed by both lawlib and PolicyEngine, and about a hundred
variables must agree on every one (up to the rounding noise of
PolicyEngine's own 32-bit floats — which lawlib, computing exactly,
gets to measure and log).
/-- `policyengine_us/variables/gov/irs/credits/earned_income/eitc.py`
policyengine-us 1.783.0, entity tax_unit, value_type float. -/
def eitc (t : TaxUnit) (d : Date) : Rat :=
(if (eitc_eligible t d) then (((min (eitc_phased_in t d)
(max 0 ((eitc_maximum t d) - (eitc_reduction t d)))) * ...Money is an exact rational, never a float — the law's arithmetic is exact decimal with statutory rounding; IEEE 754 is an implementation accident. Every generated definition carries its upstream source path and statutory citations. Parameters are dated data: one checkout computes any covered tax year.
lake build # the library, the test layer, and the theorems
lake build lawlib # the household evaluator binary
echo '{"date":"2023-01-01","tax_unit":{...}}' | ./.lake/build/bin/lawlib
| Path | What |
|---|---|
Lawlib/Core/ |
hand-written foundations: exact money and rates, dates, dated parameters, bracket scales |
Lawlib/Gen/ |
the imported core: parameters, entities, the law's formulas — regenerated from the upstream source. All changes enter through code review |
Lawlib/Verify/, Lawlib/Theorems/ |
machine-checked results about the law |
Tests/ |
everything that touches the world: the transcribed IRS table (a fixture — the law generates it), claims about printed artifacts and executed PolicyEngine, and their certified conditionals. Imports the library; never the reverse |
EXTRACTION_MANIFEST.json |
version pins, per-source hashes, the declared input boundary, date coverage |
rejection_report.md |
what the translator refused, and why — a deliverable, not a failure |
docs/ |
design, doctrine, findings |
- The printed 2023 EIC table is generated by law.
Lawlib/Verify/EicTable2023.leanholds the five-line rule (evaluate the credit formula at each $50 bracket's midpoint, anchor the phase-out at the IRS's internal unrounded endpoints, round half-up); the 10,120-cell transcription of the printed table and the proof that the rule reproduces every cell live inTests/. The smooth formula everyone models never differs from the legal (table) credit by more than $11.50 — and that bound is sharp. - The EITC has no benefit cliffs — continuity in income, an
ordinary kernel proof — with closed trapezoid forms per filing
status and number of children. The Child Tax Credit's $50 cliffs are
real, and
Lawlib/Theorems/enumerates all of them. - Two sources of law, proven 24¢ apart.
Lawlib/Verify/Catala2023.leancompares an independent, statute-first Catala encoding of §32 against the administered version and proves the statute's literal arithmetic differs from practice by exactly 24¢/50¢ — rounding the statute never mentions. Where sources of law diverge, the divergence is a theorem.
What you have to trust: symbolic theorems are ordinary kernel
proofs; whole-table computations use native_decide (adds the Lean
compiler); #print axioms is clean for the whole library. How
world-facing checks are quarantined in Tests/:
docs/categories.md.
See docs/FINDINGS.md — 20 findings so far, from PolicyEngine's float32 residue to a Lean compiler bug with a 20-line reproduction (docs/lean-fromjson-crash-repro.md).
Hand-built formalizations of law (Catala, s(CASP)) can be reasoned about but cover little; production models (PolicyEngine) cover much but can only be run. Lawlib bridges them: recover inspectable, provable structure from the largest maintained encoding of US law, faithfully or not at all. A wrong translation is worse than none — the translator rejects what it cannot express exactly, and the nightly cross-check is the trust anchor. The goal is completeness: every rule of the covered law present, exact, and provable, with the remaining gap explicitly listed.
See docs/design.md and docs/lawlib-handoff.md.
Lawlib is AGPL-3.0: the generated content derives from policyengine-us (AGPL-3.0). The pe2lean translator is separately Apache-2.0.