Formalizing US Tax Code (Using Lean): Comments

Lexifina has formalized the Internal Revenue Code within the Lean proof assistant to locate statutory drafting flaws and calculation loopholes, according to lexifina.com's report. The project builds upon earlier work verifying retirement-account rules with automated type checkers. Released under the CC0 global-law repository, the tool evaluates the official Title 26 release compiled on November 3, 2026.

This analysis details Lexifina's formalization architecture, the 138 drafting faults detected in the federal statute, and five systemic anomalies within 2025 tax rules. It also examines benchmark evaluations across 5,000 households comparing Lean against three open-source calculators. The piece is tailored for engineers and researchers tracking formal verification in law.

01Automated cross-reference verification in Title 26

The statutory text of Title 26 is published as structured XML by the House Office of the Law Revision Counsel. Lexifina built an automated parser to read internal cross-references, including text citations lacking hyperlinks like sections 922 through 927. A Lean test suite verifies whether each cited provision exists and remains in force against a git history dating to 1994.

The suite produced 257 findings cross-checked by an artificial intelligence agent against official editorial notes. The audit dismissed 98 intended transitional rules and 21 false alarms, isolating 138 genuine statutory faults. These faults include 67 obsolete references like section 1(f)(7)(A), 24 citation typos, eight level-naming mistakes, nine duplicated section numbers, and 30 unclosed parentheses.

Every drafting flaw is documented with a Lean certificate containing official XML evidence. For dead citations, the certificate proves the missing reference by cataloging all existing provisions under that heading. Lean re-checks all 138 certificates in about two and a half minutes, providing automated continuous integration for statutory updates.

02Four-part income tax formalization and proofs

Lexifina translated the individual 2025 federal income tax calculation for Form 1040 into Lean, incorporating the One Big Beautiful Bill Act of July 2025. The mathematical model breaks the computation into four distinct segments: gross income down to adjusted gross income, deductions, base tax and alternative minimum tax, and tax credits.

An artificial intelligence agent drafted code aligned with statutory phrasing before a second adversarial agent audited the implementation for overfitting. The code was tested against published Internal Revenue Service tables, worksheets, and publication examples. Lean verified mathematical proofs across every possible input, establishing that state tax caps and car-loan interest deductions never increase as income rises.

Comparing the formalization with existing tools exposed structural errors across legacy software. Tax-Calculator misallocated credits to married couples filing separately without verifying spousal separation. Additionally, UsTaxes omitted Schedule C from its 2025 returns, accidentally dropping self-employment earnings from final liability.

03Rounding contradictions and filing status anomalies

Formalizing the 2025 statute revealed that the published Code already contains six amendments taking effect in 2026. Without effective-date notes, standard models applied a 50 percent alternative minimum tax phase-out instead of 25 percent. The statute also enforces conflicting rounding directions: tips deductions drop 100 dollars per 1,000 dollars excess, while car-loan deductions drop 200 dollars per portion thereof.

The model highlighted an unintended filing status disparity regarding the state and local tax deduction cap. On joint returns, the cap shrinks by 30 cents per dollar above 500,000 dollars, but separate returns halve the cap after reduction, shrinking it by only 15 cents. Consequently, a couple earning 300,000 dollars each can deduct 25,000 dollars filing separately versus 10,000 dollars jointly.

The research proved that the official Internal Revenue Service Tax Table diverges from the statutory formula by minus five dollars to plus six dollars for incomes under 100,000 dollars. Furthermore, the statute enforces abrupt benefit cliffs: a family with three children loses an 8,046-dollar earned income credit if investment earnings exceed 11,950 dollars by one dollar.

04Benchmark tests across five thousand households

To test accuracy, Lexifina built 5,000 sample households to benchmark the Lean engine against PolicyEngine-US, Tax-Calculator, and UsTaxes. The test suite paired 2,000 standard households with 3,000 complex returns. These edge cases evaluated separate filers, students, tip and overtime earners, health savings accounts, and households earning over one million dollars with heavy investment gains.

The Lean model and PolicyEngine-US agreed on every figure for 4,993 of the 5,000 households. The remaining seven discrepancies differed by at most 11 dollars within the earned income tax credit. This variance occurred because Lean transcribed the printed Internal Revenue Service table, whereas PolicyEngine-US evaluated the underlying statutory formula.

05Calculation discrepancies in existing open-source tools

Benchmarking alternative engines against Lean exposed significant defects in established software. Tax-Calculator awarded the earned income credit and child care credits to married separate filers without verifying that spouses lived apart. On one high-earning separate return, Tax-Calculator calculated zero alternative minimum tax liability where Lean and PolicyEngine-US computed 14,881 dollars.

The UsTaxes application demonstrated 14 calculation bugs verified through household recalculations. The tool dropped self-employment income entirely by failing to attach Schedule C for the 2025 tax year. Furthermore, child-care credits failed to transfer onto the return, and dependent age tests malfunctioned.