Split Ledger

Open the tool

Overview

Split Ledger works out who should pay whom after a shared expense — a holiday, a household bill, an estate — and does it in the fewest possible payments. That last part is the point. Most bill splitters get everybody square; this one also minimises how many bank transfers it takes to get there, and can say why no shorter set exists.

The interesting part is underneath. The algorithm is written and formally proved in Lean 4: there is a machine-checked theorem saying that no list of payments which settles the same balances is shorter than the one it gives you. The page is a transcription of that algorithm into JavaScript, and it re-checks every answer against the same condition the theorem is about.

Key Features

Two ways in

  • Sheet — one line per person: name, what they paid, how many shares they carry. Right for a single bill.
  • Ledger — several expenses, each paid by a different person and split between a different subset. Right for a holiday or a long-running kitty.

Weighted shares

Shares are whole numbers, not percentages. Two people at 2 and 1 split the bill two thirds and one third; a weight of 0 leaves somebody out of that expense entirely. Percentages cannot express “three ways” without rounding, and whole shares can.

Exact money

Everything is computed in pence as integers — no floating point, so no drift. Where a total does not divide evenly the remainder is apportioned by cumulative rounding, which means the shares always add back to the total exactly and nobody is ever more than a penny from anybody else.

The fewest payments

Four people who are all out of pocket normally need three transfers. But if a subgroup happens to cancel out among themselves, they can be settled off separately and a payment is saved. Finding the most such subgroups is what makes the problem hard — it contains subset-sum — so the tool searches exhaustively up to 18 people and falls back to a good-enough method above that, saying which it used.

It checks its own answer

Every settlement carries a badge. Certified minimal means the answer passed the exact condition the Lean theorem proves implies no shorter settlement exists — and the check recomputes what it needs from the balances, so a wrong answer cannot vouch for itself.

There is no server and no account. Copy link puts the whole ledger into the address itself, so sending somebody the link sends them the ledger; they can edit their copy and send one back. Copy as form gives you the same thing as plain text, which is a fine way to paste it into a chat.

How the fewest payments are found

  1. Work out what each person paid and what their share is. The difference is their balance: positive if they are owed, negative if they owe. Balances always sum to zero.
  2. Anybody already square drops out.
  3. Look for subgroups whose balances cancel among themselves. Each one can be settled internally, and a group of n people needs n − 1 payments.
  4. So splitting k people into g such groups costs k − g payments — and the fewest payments means the most groups. That is the whole problem.
  5. Within each group, pay debtors’ balances over to creditors one at a time. Every payment clears at least one person, which is what makes n − 1 achievable.

Step 3 is the hard one, and provably so. The tool searches every subset up to 18 people, which is exact, and above that uses a greedy pass that settles everyone correctly but without the guarantee — and tells you.

What the badge does and does not mean

Does: the settlement passes Spec.certifies, the condition the Lean theorem minimal_of_certifies proves implies that no list of payments settling these balances is shorter. Money is conserved and everybody has borne exactly their share.

Does not: this page is JavaScript, not the verified binary. The proof covers the algorithm; the transcription is differential-tested against the compiled Lean on hundreds of random cases, but it remains a transcription. Above 18 people the exact search is skipped and the badge says so.

Privacy

Nothing leaves your browser. There is no server, no account and no analytics. What you type is kept in local storage on your own machine. The share link carries the ledger in the URL fragment, which browsers do not send to the server — so even the link is not visible to whoever hosts the page.

Best For

Settling up after a holiday, a house share, a group present, or an estate — anywhere several people have paid different amounts towards something and want the shortest possible list of transfers to square it up.

Limitations

  • One currency at a time; no exchange rates.
  • Above 18 people with a non-zero balance the answer is good but not guaranteed shortest.
  • No history or audit trail: it settles the position you type in, it does not keep accounts over time.

This is a living document. Last updated: October 2026