So You’re Saying There’s A Chance: FreeCell Game #11982

FreeCell deal #11982 laid out as eight columns of cards on a dark navy background, with the eight cards that can never move outlined in gold, a dashed fence labeled C around them, and the Lean theorem 'for all s, Reachable s implies not Won s'.

I have a bit of a history with Solitaire. I built my own version for WinFX back in 2005 and was still blogging about it in 2016 (granted, that was Klondike, but it’s still solitaire). So when my friend Kevin Moore sent me an Instagram reel about the one game of Windows FreeCell that nobody has ever won, game #11982, he had my attention.

Of the original 32,000 numbered Microsoft FreeCell deals, #11982 is the only one that’s never been beaten. The bit that got me was that solver programs that try every possible line of play have never found a win.

I don’t know about you, but “never found” isn’t the same as “doesn’t exist.” So I handed the transcript to my Gas City coding agents and asked them a simple question: can you solve this remaining game?

They couldn’t. Nobody can. And a couple of days later, we had a proof of that, checked by the Lean theorem prover.

Lean is a programming language for writing mathematics in a form a computer can check. Leonardo de Moura started it at Microsoft Research in 2013, and it has some serious mathematical street cred: the Liquid Tensor Experiment used it to check a theorem of Fields Medal winner Peter Scholze. More recently, it’s the tool Anthropic used to formalize Fermat’s Last Theorem. Checking my card game seemed like a reasonable thing to ask of it.

The appeal here is that my agents can write the proof and Lean can check whether it follows from the rules we’ve supplied. An agent saying “trust me, there’s no solution” is one thing; handing me a proof I can run through a separate checker is quite another. We still have to get the rules right, and there are a few details about what we’re trusting that I’ll get to.

Here’s how we proved game #11982 can’t be won.

The Deal Is Just Arithmetic

FreeCell started life when Paul Alfille implemented it on the PLATO system. The Windows version you remember is Jim Horne’s. He wrote a DOS version, then joined Microsoft and brought it to Windows. Horne’s clever bit was making every deal a number. Type in 11982 and you get those 52 cards in those exact places in the Microsoft deal layout, because the shuffle is nothing but the random number generator from Microsoft’s C runtime, seeded with the game number:

x_0 = 11982, \qquad x_{k+1} = (214013\,x_k + 2531011) \bmod 2^{31}, \qquad r_k = \left\lfloor \frac{x_{k+1}}{2^{16}} \right\rfloor

The deck starts in order (A♣ A♦ A♥ A♠ 2♣ … K♠). On each of the 52 steps, the game takes the next random number, picks the card at index

j_k = r_k \bmod (52 - k), \qquad k = 0, 1, \dots, 51,

deals it, and fills the hole with the last card in the deck. Cards go out left to right in rows of eight, so the first eight cards dealt end up at the bottom of the columns. Run that for game #1 and you get the famous J♦ 2♦ 9♥ J♣ opening. Run it for game #11982 and you get this:

The deal for game 11982 as eight columns. Column 1: A♥ 3♦ K♦ J♣ 6♣ J♦ K♣. Column 2: A♠ 3♥ 6♥ 5♦ 2♣ 7♦ 8♦. Column 3: 4♥ Q♠ 5♠ 5♣ 10♥ 8♥ 2♠. Column 4: A♣ Q♣ 4♦ 8♣ Q♥ 9♣ 3♠. Column 5: 2♦ 8♠ 9♥ 9♦ 6♦ 2♥. Column 6: 6♠ 7♥ J♥ 10♦ 10♣ Q♦. Column 7: 10♠ A♦ 9♠ K♥ 4♠ 4♣. Column 8: J♠ K♠ 3♣ 7♣ 7♠ 5♥. Eight cards are highlighted in gold as never moving: A♠, 3♥, 6♥, 4♥, Q♠, A♣, Q♣ and 6♠.

Three of the aces are at the bottom of their columns under six cards each, and the fourth is under four. Those gold cards are a spoiler for later in the post: they’re the cards that never move, no matter what you do.

First, the Obvious Thing

The agents started by writing the deal generator, checking it against game #1, and then writing an exhaustive solver in C++: a depth-first search over single-card moves that remembers every position it’s seen so it never explores one twice. It solved game #1 in about 27,000 positions. On #11982 it ran out of positions to try after 61,643. No win.

That number surprised me. I’d assumed #11982 was a long, subtle game that you lose at the very end. It’s the opposite. The whole universe of positions you can ever reach from that deal is tiny, and in every single one of them, you’ve gotten at most two cards to the foundations. Not two suits. Two cards.

Then I asked my agents to turn things up to eleven.

They found that the game is one favor away from winnable. If you could hold a single card in your hand for one move while all four free cells are full, the whole deal falls open. With a fifth free cell, it’s winnable outright. But I’d told them no cheats and no relaxed rules. Under the real rules, it was exhaustive search or nothing.

Is Exhaustive Search Even a Proof?

Yes, exhaustive search counts. Mathematicians leaned on proof by exhaustion for the four color theorem in 1976. If you can enumerate every case and check each one, you’ve proved the claim. The catch is that you have to trust the program that did the enumerating.

And trusting the program is what the history of #11982 rests on. Dave Ring’s Internet FreeCell Project got over a hundred volunteers to solve 31,999 of the 32,000 deals by hand in 1994 and 1995. On November 1, 1995, Scott McCarter at HP emailed in the results of a breadth-first search he’d written over several lunchtimes:

What finally happened?
  NO SOLUTION FOUND
  num of hands explored             73600
  most cards moved to "suit" area       2

That “2” matches the ceiling our search found 31 years later with completely different code. McCarter was also honest about it: “The program may have defects in it. I would not be surprised,” he wrote, and the archived email doesn’t include his source code. (McCarter’s email, preserved by the Wayback Machine.)

Since then, a lot of solvers have failed on #11982. The Freecell Solver FAQ lists eleven of them. But “eleven programs agree” is still evidence, not proof, and the folks who maintain Freecell Solver know it. Their to-do list says that the exhaustive solvers that traversed the deal’s game graph were never “implemented using a proof assistant which verified and validated its correctness proof,” and that “we would like to see such a solver written.”

So we tackled the #11982 part of that request. We didn’t prove a general solver correct but we did build a checkable proof that this particular deal can’t be won, and then submitted it to the nice Freecell Solver folks.

Stating the Theorem

Before Lean can check anything, you have to say precisely what “can’t be won” means. A position is the eight columns, the contents of the four free cells, and how high each foundation is:

s = (\,c_1, \dots, c_8;\ F;\ h\,), \qquad c_i \in \mathrm{Card}^{*}, \quad F \subseteq \mathrm{Card},\ |F| \le 4, \quad h \in \{0,\dots,13\}^4

The free cells are a set because they’re interchangeable: a 9♣ in the first cell is the same position as a 9♣ in the third. The rules boil down to two predicates. A card x can go on a column whose top card is p, or onto its foundation, when

\mathrm{stack}(x, p) \iff \mathrm{rank}(p) = \mathrm{rank}(x) + 1 \ \wedge\ \mathrm{red}(p) \ne \mathrm{red}(x), \qquad \mathrm{home}(x, h) \iff h_{\mathrm{suit}(x)} + 1 = \mathrm{rank}(x)

Add “any card can go on an empty column” and “a card from a column can go into a free cell if one is open,” and you have moves(s), the set of positions one legal move away from s. The reachable positions are the smallest set that contains the opening deal s₀ and is closed under moves:

\mathcal{R} \;=\; \bigcap \left\{\, X \subseteq \mathcal{S} \;\middle|\; s_0 \in X \ \wedge\ \forall s \in X,\ \mathrm{moves}(s) \subseteq X \,\right\}

A position is won when every foundation is up to the king, and the theorem says no reachable position is won:

\mathcal{W} = \{\, s \mid h(s) = (13, 13, 13, 13) \,\}, \qquad\qquad \mathcal{R} \cap \mathcal{W} = \varnothing

But wait, you say, real FreeCell lets you move a whole run of cards at once. It does, as long as the run has at most

k \le (f + 1) \cdot 2^{e}

cards, where f is the number of empty free cells and e the number of empty columns available for temporary storage, excluding the destination column. That limit exists because a “supermove” is just shorthand for a sequence of single-card moves through the free cells and empty columns. It can’t reach a position that single moves can’t, so modeling single moves loses nothing. (We checked that too. Adding supermoves to the solver reached the identical 61,643 positions.)

The Trick: Don’t Verify the Search, Verify the Answer

This is the part I find elegant. Proving a 100-line search algorithm correct in Lean would be a real slog: termination, hash set invariants, the whole bit. So we don’t. Instead, the search just proposes an answer, a set C of positions, and Lean checks three easy things about it.

s_0 \in C, \qquad \forall s \in C,\ \mathrm{moves}(s) \subseteq C, \qquad C \cap \mathcal{W} = \varnothing

If all three hold, we’re done, because of one small lemma:

s_0 \in C \ \wedge\ \bigl(\forall s \in C,\ \mathrm{moves}(s) \subseteq C\bigr) \;\Longrightarrow\; \mathcal{R} \subseteq C

The proof is induction on how a position got reachable. There are only two ways: it’s the deal, or it’s one move away from something reachable. Both cases land in C:

\frac{}{\;s_0 \in C\;}\ (\text{deal}) \qquad\qquad \frac{s \in C \qquad t \in \mathrm{moves}(s)}{t \in C}\ (\text{step})

So every reachable position is in C, nothing in C is won, and therefore nothing reachable is won. Mathematicians would call C an inductive invariant. I think of it as a fence: start inside, and there’s no legal move that takes you outside.

Two diagrams side by side. On the left, a dashed gold fence labeled C encloses a graph of positions including the starting deal, with every edge staying inside and the Won position outside, captioned C intersect Won is empty. On the right, a similar fence where one red arrow escapes from a position inside to a point outside, captioned moves of s is not a subset of C.

The nice thing about a fence is that it doesn’t matter how sloppy the search was. If it missed a position, some legal move will escape the fence and the check fails. If it added junk, the junk has to be closed under moves too, and it still can’t contain a win. The search can be as buggy as it likes; it can’t make the check pass for a deal that has a win.

Walking Through the Lean

The whole thing is one Lean 4 file of about 150 lines. Here’s how the pieces fit together:

The top band is the part you have to read and believe. Everything else is either checked by Lean or doesn’t matter.

The deal

Lean doesn’t take my word for the cards. It regenerates them from the game number with the same arithmetic as above:

/-- MSVC `rand()`: seed ← seed·214013 + 2531011 (mod 2³¹), output seed / 2¹⁶. -/
def lcg (seed : Nat) : Nat := (seed * 214013 + 2531011) % 2 ^ 31

def dealOrder (game : Nat) : List Card := Id.run do
  let mut deck : Array Card := (List.range 52).toArray.map fun i => ⟨i / 4 + 1, i % 4⟩
  let mut seed := game
  let mut out : Array Card := #[]
  for _ in [0:52] do
    seed := lcg seed
    let j := (seed / 2 ^ 16) % deck.size
    out := out.push deck[j]!
    deck := deck.set! j deck.back!   -- fill the hole with the last card
    deck := deck.pop
  return out.toList

def deal : State := { cols := msDeal 11982, cells := [], home := [0, 0, 0, 0] }

The file prints game #1 as a sanity check, and it starts J♦ 2♦ 9♥ J♣, just like it did on your Windows 95 box.

The rules

moves is the heart of the trusted part, so it’s written to be read: take a card off the top of a column or out of a free cell, then try every place it could go.

def canStack (c parent : Card) : Bool := parent.rank == c.rank + 1 && parent.red != c.red
def canHome (home : List Nat) (c : Card) : Bool := home.getD c.suit 0 + 1 == c.rank

def moves (s : State) : List State :=
  let fromCols : List (Card × State × Option Nat) :=
    (List.range 8).filterMap fun i =>
      match s.cols.getD i [] with
      | [] => none
      | c :: rest => some (c, { s with cols := s.cols.set i rest }, some i)
  let fromCells : List (Card × State × Option Nat) :=
    s.cells.map fun c => (c, { s with cells := s.cells.erase c }, none)
  (fromCols ++ fromCells).flatMap fun (c, s', src) =>
    -- to its foundation
    (if canHome s.home c then [{ s' with home := s'.home.set c.suit c.rank }] else []) ++
    -- onto an empty column, or onto a card one higher of the opposite colour
    ((List.range 8).filterMap fun j =>
      if src == some j then none else
      match s'.cols.getD j [] with
      | [] => some { s' with cols := s'.cols.set j [c] }
      | p :: ps => if canStack c p then some { s' with cols := s'.cols.set j (c :: p :: ps) } else none) ++
    -- from a column into a free cell
    (if src.isSome && s'.cells.length < 4 then [{ s' with cells := insertSorted c s'.cells }] else [])

Notice what’s not there: no moves off the foundations, which matches Microsoft’s rules. (We also checked what happens if you allow them: the deal still can’t be won, and at most two cards ever reach the foundations.) Reachability and winning are then stated directly, as an inductive definition that mirrors the two rules above:

inductive Reachable : State → Prop
  | deal : Reachable deal
  | step {s t : State} : Reachable s → t ∈ moves s → Reachable t

def Won (s : State) : Prop := s.home = [13, 13, 13, 13]

The check and the lemma

checkCert is the three conditions from the fence, written as a function that returns a Bool:

def checkCert (c : HashSet State) : Bool :=
  c.contains deal && c.toList.all fun s => !won s && (moves s).all c.contains

And cert_sound is the induction, which Lean’s kernel checks in full:

theorem cert_sound (c : HashSet State) (h : checkCert c = true) :
    ∀ s, Reachable s → c.contains s = true ∧ won s = false := by
  simp only [checkCert, Bool.and_eq_true, List.all_eq_true, Bool.not_eq_true'] at h
  obtain ⟨hdeal, hall⟩ := h
  have key : ∀ s, c.contains s = true → won s = false ∧ ∀ t ∈ moves s, c.contains t = true := by
    intro s hs
    have := hall s (HashSet.mem_toList.mpr (HashSet.mem_iff_contains.mpr hs))
    exact this
  intro s hr
  induction hr with
  | deal => exact ⟨hdeal, (key _ hdeal).1⟩
  | step _ ht ih =>
    have hc := (key _ ih.1).2 _ ht
    exact ⟨hc, (key _ hc).1⟩

The deal case and the step case are exactly the two inference rules from earlier.

The search and the big check

explore is an ordinary depth-first search with a hash set. Lean doesn’t care whether it’s right; it only cares about what it hands back:

def certificate : HashSet State := explore 10000000

theorem certificate_ok : checkCert certificate = true := by native_decide

theorem freecell_11982_unwinnable : ∀ s, Reachable s → ¬ Won s := by
  intro s hr hw
  have := (cert_sound certificate certificate_ok s hr).2
  simp [won, Won] at *
  simp [hw] at this

The certificate holds 84,767 positions. That’s more than the 61,643 the C++ solver saw, because the Lean version keeps the columns in fixed places instead of treating a rearrangement as the same position, and it doesn’t play cards home automatically.

What You Still Have to Trust

No proof is trust-free, so here’s the honest list. When you ask Lean what the final theorem rests on, it says:

'freecell_11982_unwinnable' depends on axioms: [propext,
 Classical.choice,
 Quot.sound,
 certificate_ok._native.native_decide.ax_1_1]

The first three are Lean’s standard axioms. The fourth is the price of speed: native_decide evaluates checkCert by compiling it and running the compiled code, rather than having the kernel grind through 84,767 positions one reduction step at a time. So you’re trusting Lean’s compiler for that one step. The induction, the theorem statement and everything connecting them are checked by the kernel.

The other thing you have to trust is the spec: msDeal, moves, Reachable and Won. If moves were missing a legal move, the proof would be a perfectly valid proof of the wrong thing. So we tested the spec from the other direction:

The same rules win games that are winnable. Using that exact moves, a search found wins for games #1, #617 and #1941.
The check isn’t a rubber stamp. Deleting the deal, its first successor or its last successor from the certificate makes checkCert return false every time.
The deal is the real deal. Lean’s msDeal 1 matches the published game #1, and msDeal 11982 matches the layout above.

Why It’s Stuck

A machine-checked proof tells you that the game is lost. It doesn’t tell you why, and I wanted the why. We’d already found that the black aces never get free. Across every reachable position, the Q♣ sitting on the A♣ never moves, and neither does the 6♥ two cards above the A♠. No black ace means no clubs or spades on the foundations, which means no win.

Even better, the Q♣ is uncovered in only 8 of those positions, and they all look like this:

A position with all four free cells full (3♠, 9♣, 8♣, 4♦), empty foundations, and column 4 dug down to A♣ with Q♣ exposed and highlighted. Q♥ sits on K♣ at the end of column 1. The two red kings, K♦ in column 1 and K♥ in column 7, are tinted to show they are buried.

In this one, digging down to the Q♣ meant parking the 3♠, 9♣, 8♣ and 4♦, and every card they could legally sit on is buried, so they used up all four free cells. Now the Q♣ needs a free cell, an empty column or an exposed red king, and there aren’t any. The other seven positions are variations on that squeeze. The whole deal fails by one space, which is why a fifth free cell fixes it.

I also asked for a proof a human could check without running a program, and that’s where we failed. The natural approach is to count parking spaces at the moment one of the frozen cards is about to move:

\underbrace{4}_{\text{free cells}} \;+\; \underbrace{V}_{\text{emptied columns}} \;\ge\; \underbrace{P}_{\text{parked cards}} \;+\; 1

For this attempt, we considered candidate arrangements without requiring that a legal sequence of moves could reach them. That makes this a larger set than the reachable positions counted earlier. For each of three target cards, Q♣, Q♠ and 6♥, we considered about a million candidate arrangements. With no emptied columns (V = 0), none allowed the target card to escape. But with exactly one emptied column, counting alone allows between 24 and 136 arrangements (depending on the card) where it could escape, and ruling those out means following the actual order of moves. At that point you’re doing the exhaustive search again, just by hand. We looked for a slicker invariant that sidesteps the move order and didn’t find one.

Has Anyone Done This Before?

I couldn’t find anyone that had done this kind of formal proof for this elusive game of FreeCell. Lots of people have searched #11982 exhaustively, including McCarter in 1995, and Freecell Solver lists eleven programs that come up empty. There’s a Lean 4 FreeCell project that calls itself verified, but its theorems check the deck size and a stacking rule, rather than proving anything about a particular deal. I couldn’t find a Coq, Isabelle or Lean proof about #11982 anywhere, and Freecell Solver’s broader request for a verified solver is still on its to-do list. If you know of an earlier machine-checked proof, please let me know. I’d love to give credit where it’s due.

A reel about a 30-year-old card game turned into a few days of writing solvers, failing at a hand proof and learning more Lean than I wanted to. The answer is still the one Dave Ring’s volunteers came up with in 1995. What I hadn’t expected was that I could work with coding agents to produce a formal proof of it. They couldn’t win the game, but they could help prove that nobody can.

OpenAI, Anthropic and Google have been going on about what their models can do for mathematics. OpenAI is publishing new mathematical results with Lean formalizations, Anthropic has formalized Fermat’s Last Theorem with Claude, and Google reports that AlphaEvolve is helping solve Erdős problems and improve mathematical bounds. It’s fun to find that I can do my little part in the math world, too. Naturally, mine involves Solitaire. : )

Download the Lean proof and run lean FreeCell11982.lean with Lean 4.35 to check it yourself. Enjoy.