A General Library of Legal Components
summary
An exploratory library implements composable, verifiable legal components in Lean 4, encoding tax rules (notably section 1031 and section 121) plus an implementation of form 8824 and operational semantics for civil procedure. Definitions are decidable so code runs like boolean checks; the repo proves equivalence and divergence between US Code, CFR and IRS worksheets, uses Treasury regulation examples as counterexamples, and produces both ordinary and non‑deterministic competing tax results ordered by authority. Many proofs are finished but full maintenance and mathlib porting remain unresolved.
AI-written summary · about
chapters (6)
- 0:00Introduction
- 1:10A General Library of Legal Components
- 2:21Tax Concept
- 9:04Booleans
- 14:18Civil Procedure
- 16:32QA
related talks
22mThe Lean Mathematical Library
50mProgramming The Law: Best Practices
01h 04mLean4Lean: Mechanizing the Metatheory of Lean
19mPanel: Compilation Frameworks
20mImplementation and Synthesis of Math Library Functions
01h 06mVerifying a compiler through equational means
53mSemantics-based program manipulation in the age of LLMs
31mA Coq Library of Undecidable Problems