LegalLean

Verified legal reasoning, from natural language to formal proof.

LegalLean formalises legal rules as machine-checkable propositions in Lean 4. The signature framing: large language models are heuristic transducers; Lean 4 is the invariant verifier. The boundary between what can and cannot be formalised is itself encoded in the type system.

80+

machine-checked theorems

case studies

automated pipelines

The architecture

Three layers that validate their own thesis.

The process of writing the monograph is itself an instance of the claim it makes: that legal reasoning can be partially formalised in dependent type theory.

Layer 1 · Lean 4Verified types and proofs — the invariant verifier.
Layer 2 · JSON IRA claim-evidence graph with defeat relations.
Layer 3 · ProseThe published monograph, generated from both layers.

 -- A defeasible legal rule: holds unless defeated. structure LegalRule where
premises   : List Prop
  conclusion : Deontic
  defeaters  : List Defeat
-- Open texture is a first-class type, not a gap. class RequiresHumanDetermination (p : Prop)
theorem mortgage_interest_deductible
    (h : qualifiedResidenceInterest x) :
    DefeasiblyHolds (deduct x) := by
exact irc163h_rule h
✓ checked under IRC §163(h) 

The type system

Legal concepts as dependent types

Type	Purpose
`Deontic`	Permitted / prohibited / obligatory
`LegalRule`	A rule carrying defeasibility metadata
`EvidenceFor`	Propositions-as-types for legal evidence
`DefeasiblyHolds`	Non-monotonic entailment — holds unless defeated
`FormalisationBoundary`	Hart's open texture as a first-class type
`RequiresHumanDetermination`	Marks where formal verification yields to human judgment
`Vague`	Core / penumbra distinction
`Discretionary`	Authority discretion

The crucial move: FormalisationBoundary and RequiresHumanDetermination encode, inside the type system, exactly where formal verification stops and human judgment begins.

Case studies

From statute to proof

IRC §163(h)

Complete

Mortgage interest deduction, formalised to Lawsky's gold standard. The reference case showing the method end-to-end.

O-1 Visa

Research

The "3 of 8" extraordinary-ability criteria modelled as dependent types — satisfaction is a typed proof obligation.

Australian TCP Code

Research

Telecommunications regulatory compliance, benchmarked against Governatori's defeasible-logic formalisations.

Automated pipeline

Research, then prove.

Research · Perplexity

Extracts sorry / TODO stubs from the Lean files, generates prompts shaped to match LegalLean types, and queries a model council. Conditions map to rule conclusions, exceptions to defeaters, vague terms to formalisation boundaries.

Prove · Aristotle

An IMO gold-medal-level engine fills the sorry stubs with verified Lean 4 proofs, running files in parallel. What the research pipeline opens as a question, the prover closes as a machine-checked theorem.

This is what "trustworthy AI" should mean.

Not a confident answer, a checkable proof, and an honest boundary where judgment takes over.

See the full Stack → Speak to us