When Math Meets Policy: Formalizing Indian Tax Logic

Filing taxes is an excruciatingly long and complex process - largely because tax laws themselves are dense and difficult to parse. Yet, every single tax filer is expected to understand these rules and report their income flawlessly. The penalty for getting it wrong is a fine in the best-case scenario, and jail time in the worst.

This problem is so ubiquitous that we started calling incredibly demanding tasks "taxing."

Even the most advanced AIs of today (Claude, GPT, et al.) can’t help you much with filing taxes either! As the New York Times noted, A Word to the Wise: Don’t Trust A.I. to File Your Taxes. 

Current AI systems are trained to predict the most likely next word, outputting an answer that is only roughly correct. But "roughly correct" is a disaster when filing taxes. Every single declaration in your return needs to be exact; if just one number is wrong, the entire return is invalid. This fundamental limitation means standard LLMs will likely never be reliable enough to handle your taxes independently. You need a fundamentally different approach.

At Pramaana Labs, we chose to tackle this problem by formalizing tax logic.

What Did We Formalize?

At its core, formalization means translating complex, real-world rules into strict, machine-readable mathematical code. For this project, we took the actual computations of the ITR-2 tax form and mapped its dense web of fields and dependencies into runnable, verifiable programs.

To build this, we chose Lean.

Unlike standard programming languages that simply execute logic and spit out an answer, Lean is an interactive theorem prover. It allows us to write the ITR-2 computations and simultaneously prove mathematical properties about them. With Lean, we can mathematically guarantee that a specific set of inputs produces exactly one valid tax output. We can prove that a tax rule holds true across every possible income permutation, or conversely, prove that an edge case exists.

This ability to provide absolute, mathematical guarantees of correctness is exactly what makes Lean the perfect choice for formalizing zero-margin-of-error domains like taxes.

Why Formalize?

For Tax Filers

There are plenty of online calculators that estimate the amount of tax owed, but the onus remains on the filer to understand which laws apply to them and how to report those numbers. Formalizing the entire tax law shifts that burden. The user no longer needs to hunt for applicable deductions; the system systematically identifies and applies them. More importantly, it can mathematically prove it has found the maximum possible deduction for that specific scenario. Because the system relies on proofs, it can transparently explain exactly how every number was derived.

For Policy-makers

Tax laws change continuously. Lawmakers want to ensure new changes don't introduce unintended consequences or loopholes that enable tax evasion. By formalizing the tax code, policy-makers can mathematically prove whether two versions of a tax law are identical in specific scenarios, or easily identify exactly who will pay more or less under a new proposal. They can also prove - or disprove - if the new tax laws are fundamentally fair.

One such property of fairness is Monotonicity. In the context of tax laws, monotonicity means this: All else being equal, an increase in your gross salary should never result in a decrease in your net (take-home) pay.

Proving (or Disproving) Monotonicity for Indian Tax

Before starting out, we expected the Indian tax laws to be monotonic. Even though the system uses strict slabs and surcharges, there is a built-in provision called "Marginal Relief" designed to prevent this exact problem.

However, when we formalized the Indian tax laws and asked our system to prove monotonicity, we were surprised by what it found.

Consider this scenario:

At 50 lakhs taxable income, total tax liability is Rs. 11,23,200. So, your net pay is Rs. 38,76,800

However, at 51 lakhs taxable income, total tax liability is Rs. 12,27,200. So, your net pay is Rs. 38,72,800.

Even though your taxable income increased by Rs. 1,00,000, your take-home pay actually dropped by Rs. 4,000.

Therefore, the current tax system is not monotonic. In fact, our system proved that the maximum loss penalty happens around the 2 Cr boundary, where a taxpayer can lose as much as Rs. 36,416 just by earning slightly more.

How to fix it?

One of the major benefits of formalization is absolute visibility; we know exactly how every number in that faulty calculation was derived. Because of this, we were able to ask our system the inverse question: What is the root cause of this penalty, and what is the exact fix?

The system identified the flaw immediately. The error stems from how marginal relief and "cess" (a specific tax surcharge) interact. Currently, relief is only applied to the surcharge component, but the cess is computed on the total tax owed prior to relief. Because you don't get marginal relief on the additional cess, that exact discrepancy causes your take-home pay to drop.

The fix is straightforward: include the cess as part of the marginal relief calculation.

To test this, we edited our formalized tax law to include the additional cess in the marginal relief block. When we asked our system to prove monotonicity on the updated code, it successfully proved it.

This perfectly illustrates how formalization does more than just clarify computations. It enables us to prove policy properties, uncover hidden flaws, and systematically identify the exact legislative changes needed to make our laws function as intended.