Find the lowest federal income tax you can legally pay

Z3, a theorem prover, checks every legal combination of moves and returns the lowest tax it can prove.

Household

Filing status

State

Your age

Spouse's age

Children under 17

Other dependents

I'm legally blind My spouse is legally blind

Dependent care and education

Dependent care paid

People cared for

Tuition and fees

Students

529 balance

My employer offers a dependent care FSA

Income and tax paid

Your wages

Spouse's wages

Self-employment

Pass-through business

Interest

Qualified dividends

Pensions, rents, other income

Federal withholding

Estimated payments

The business is a professional service (law, medicine, consulting)

Investments

Unsold long-term gain

Cash you must raise

Unsold losses

Short-term gains taken

Loss carryforward

Deductions

Mortgage interest

State and local taxes

Medical expenses

Student loan interest

Planned giving

Stock you could give

Accounts you can use

401(k) or similar workplace plan Spouse has one too Plan offers a Roth 401(k) Covered by a workplace retirement plan High-deductible health plan (HSA)

Compare joint and separate filing

Your minimum

Lowest tax the solver can prove

No planning

With this plan

Effective rate

Filing as

What to do

What each move saves

Extra tax if you skip that move.

Filing status
Status	Tax

Worth knowing

How the tax adds up
Line	Amount

Capital gains by rate
Rate	Gain

Where each number comes from
Item	Source	Value