Présentation

Le projet, mené par l’initiative global‑law, traduit l’ensemble du Title 26 du US Code dans le langage de preuve Lean. Lean agit comme un vérificateur de type : chaque définition et chaque référence doit être justifiable à partir du texte officiel. En s’appuyant sur la version du Code publiée le 3 novembre 2026, les auteurs ont identifié 138 erreurs de rédaction dans le texte législatif.

Méthodologie

Un parseur lit chaque renvoi croisé (ex. « paragraph (2) of subsection (b) », « sections 922 through 927 ») et génère une suite de tests exécutée par Lean. Sur la base de la même version, la suite a produit 257 constats : 98 étaient prévus (règles rétroactives ou dispositions en attente), 21 de faux positifs liés aux hyperliens de l’éditeur, et 138 véritables fautes. Chaque faute possède un certificat Lean qui montre la référence manquante ou obsolète, et le re‑check complet dure environ deux minutes et demie. Le code source du Code fiscal est conservé dans un dépôt Git, un commit par loi publique, ce qui permet de remonter chaque anomalie à son texte d’origine depuis 1994. Pour la modélisation du calcul d’impôt 2025, l’équipe a utilisé l’IA afin de traduire les articles en Lean, puis a soumis chaque module (revenus, déductions, impôt, crédits) à trois logiciels fiscaux indépendants sur 5 000 foyers. Un second agent IA a revu chaque partie de façon adversariale afin de détecter les écarts entre le texte et le code.

Résultats et anomalies

Le modèle Lean a mis en lumière cinq incohérences majeures : (1) le Code consolidé mélange les amendements de 2025 et de 2026, entraînant un calcul d’AMT à 50 % au lieu de 25 %; (2) les nouvelles déductions pour pourboires et heures supplémentaires sont arrondies à la baisse de 100 $ par tranche de 1 000 $, alors que la déduction de prêt automobile augmente de 200 $ par tranche de 1 000 $, créant un déséquilibre de 1 $ ; (3) le plafond SALT diminue de 30 cents par dollar au‑delà de 500 k $ en déclaration conjointe, mais ne chute que de 15 cents lorsqu’on déclare séparément, ce qui permet à un couple gagnant 300 k $ chacun de déduire 25 k $ au lieu de 10 k $ ; (4) la Tax Table de l’IRS diffère de la formule légale de –5 $ à +6 $ pour tout revenu imposable inférieur à 100 k $, ce qui a été prouvé pour chaque tranche et chaque statut ; (5) des seuils de bascule provoquent des pertes abruptes : un revenu d’investissement de 11 951 $ annule l’intégralité du crédit EITC, soit une perte de 8 046 $, et le crédit d’épargne chute de 2 000 $ à 800 $ dès 47 501 $ de revenu.

Implications et limites

Lean fournit une preuve exhaustive couvrant chaque entrée possible, ce qui élimine les erreurs de logique détectées dans Tax‑Calculator (EITC appliqué à des couples séparés) et UsTaxes (absence de Schedule C). Le processus est peu coûteux : un nouveau relevé du Code déclenche automatiquement la suite de tests et signale les nouvelles fautes. Cependant, la traduction initiale du texte en Lean reste sujette à perte d’information, dépendant de la qualité de l’IA. De plus, la vérification ne couvre que les incohérences textuelles ; les choix de politique fiscale ou les interprétations jurisprudentielles restent hors de portée. Malgré ces limites, la démarche montre que la formalisation automatisée peut repérer des bugs législatifs et des « loopholes » invisibles aux contrôles humains.