Yesterday, we verified that known tax loopholes could be identified using a Lean search. Today, we set out to formalize the entire Internal Revenue Code to hunt for unknown loopholes (bugs).
This work is part of global-lawglobal-law, a CC0 repository of versioned legislation and case law.[3] Our argument is that pointing AI and a proof checker at a versioned record of the law finds the contradictions and mechanical mistakes that people miss. In particular, we can catch mistakes in the text, and see what the rules allow, including what they allow by accident. To do so, we translated each section of the law into Lean, staying close to the statute’s own words, and tested it against the worked examples the IRS prints in its forms and instructions.
