A Vericoding Exercise

Eric Rothstein Morris

2026-10-01

LeetCode 1171, with a specification and a proof in Lean.

In September 2026, OpenAI reported that about 10,000 of its AI agents had found a singularity in the three-dimensional Navier–Stokes equations, the subject of one of the Millennium Prize Problems, and that another AI model had formalised the proof in Lean, which checked it (Quanta Magazine). Mathematicians are still examining the result, and who deserves credit is disputed. I wondered: if AI is this capable, why does vibe coding still produce buggy code?

Most of the advice I found was to review the code that AI writes more carefully and to test it better. Given my background in formal methods, I asked a different question: why not have the AI go the extra mile and prove that its code is correct? This idea already has a name, vericoding: an AI writes code from a formal specification, together with a proof that the code meets it, and a machine checks the proof (Bursuc et al., 2025). Lean is both a programming language and a theorem prover, so it can play both parts.

This post is a small experiment in that spirit. Together with Claude Code, Anthropic's coding assistant, I wrote a specification for a LeetCode problem in Lean. Claude then wrote a solution and a proof that it meets the specification, and Lean checked the proof.

An Exercise in Vericoding

The problem we study is LeetCode 1171: Remove Zero Sum Consecutive Nodes from Linked List: given the head of a linked list of integers, we must repeatedly delete a consecutive sequence of numbers that adds up to zero, until no such sequence remains. For example, the list [1, 2, -3, 3, 1] can reduce either to [3, 1] or to [1, 2, 1].

A small simplification for this blog entry: LeetCode's input is a linked list whose nodes can be changed, and solutions relink the nodes to cut runs out. We use Lean's List instead.

The Specification

Since we are vericoding, we should first try to capture the specification formally.

/-- `t` results from `s` by deleting runs that sum to zero. Read `s` from
the left: each element is either kept, or starts a run that sums to zero
and is deleted. Core Lean's `List.Sublist` is defined the same way, except
that it may delete any element. -/
inductive DeletesZeroSumRuns : List Int → List Int → Prop
  | nil : DeletesZeroSumRuns [] []
  | keep (a : Int) (s t : List Int) : DeletesZeroSumRuns s t → DeletesZeroSumRuns (a :: s) (a :: t)
  | delete (w s t : List Int) : w.sum = 0 → DeletesZeroSumRuns s t → DeletesZeroSumRuns (w ++ s) t

/-- LeetCode 1171 for one input `s` and output `t`: `t` has the sum of
`s`, results from `s` by deleting runs that sum to zero, and has no run
other than `[]` that sums to zero. `w <:+: t` says that `w` is a run of
`t`: `t = u ++ w ++ v` for some `u` and `v`. -/
def RemoveZeroSumSpec
  (s t : List Int)
  : Prop :=
  t.sum = s.sum ∧
  DeletesZeroSumRuns s t ∧
  ∀ w, w <:+: t → w ≠ [] → w.sum ≠ 0

/-- A function solves LeetCode 1171 if it meets the spec on every input. -/
def SolvesLeetCode1171
  (f : List Int → List Int)
  : Prop :=
  ∀ s, RemoveZeroSumSpec s (f s)

We had several back-and-forth interactions with Claude Code to find a proper specification. This is probably the hardest of the tasks: simpler conditions are too weak; conditions on sums alone would allow a function to turn [1, 2] into [3]; it must support several deletions of zero-sum runs, and the output must have no zero-sum run of its own.

From that specification, it was relatively easy for Claude to find a candidate function:

def removeZeroSumSublists
  (s : List Int)
  : List Int :=
  match s with
  | [] => []
  | a :: rest =>
    /- `rest.scanl (· + ·) a` lists the sums of the nonempty prefixes of
    `a :: rest`; `j` is the position of the first that is zero. -/
    match (rest.scanl (· + ·) a).findIdx? (· == 0) with
    /- The first `j + 1` elements sum to zero: delete them. -/
    | some j => removeZeroSumSublists (rest.drop j)
    /- No nonempty prefix sums to zero: keep `a`. -/
    | none => a :: removeZeroSumSublists rest
  /- Lean accepts a recursive function only if it can see that the
  recursion ends. `termination_by` names a number that decreases at each
  call: both calls are on lists shorter than `s`. -/
  termination_by s.length

Lean accepts the solution only with termination_by s.length, which tells it why the recursion ends: on its own, it can't see that rest.drop j is shorter than s.

We can run a quick test,

[3, 1]#eval removeZeroSumSublists [1, 2, -3, 3, 1]

[3, 1]

but we should focus our efforts on proving the goal SolvesLeetCode1171 removeZeroSumSublists. To do so, Claude suggested proving a couple of facts before. These facts are related to the expressions used in the implementation of removeZeroSumSublists.

One of the most fascinating advantages about doing vericoding for the average developer is that they don't need to be too careful about the proofs generated by AI; as long as those proofs "don't cheat" (i.e., they don't say sorry or use "cheating axioms"), they are valid, and any valid proof of the specification suffices! In that spirit, I invite you to skip the next section and continue at section The Goal; unless you are curious about the lemmas that Claude proposed.

Lemmas

sum_cons_eq_foldl says that the sum of a :: l is l folded with +, starting from a, which is how scanl computes it. The proofs below need it to read the sums that removeZeroSumSublists checks as sums of prefixes.

/-- The sum of `a :: l` is `l` folded with `+`, starting from `a`: the
form in which `scanl` gives the sums of prefixes. -/
theorem sum_cons_eq_foldl
  (a : Int)
  (l : List Int)
  : (a :: l).sum = l.foldl (· + ·) a := bya:Intl:List Int⊢ (a :: l).sum = List.foldl (fun x1 x2 => x1 + x2) a l
  rw [List.sum_eq_foldla:Intl:List Int⊢ List.foldl (fun x1 x2 => x1 + x2) 0 (a :: l) = List.foldl (fun x1 x2 => x1 + x2) a l]a:Intl:List Int⊢ List.foldl (fun x1 x2 => x1 + x2) 0 (a :: l) = List.foldl (fun x1 x2 => x1 + x2) a l
  simpAll goals completed! 🐙

DeletesZeroSumRuns.sum_eq says that deleting runs that sum to zero keeps the sum of a list. It gives the sum part of the specification.

/-- Deleting runs that sum to zero keeps the sum. -/
theorem DeletesZeroSumRuns.sum_eq
  {s t : List Int}
  (h : DeletesZeroSumRuns s t)
  : t.sum = s.sum := bys:List Intt:List Inth:DeletesZeroSumRuns s t⊢ t.sum = s.sum
  induction h with
  | nil =>nils:List Intt:List Int⊢ [].sum = [].sum rflAll goals completed! 🐙
  | keep a s t _ ih =>keeps✝:List Intt✝:List Inta:Ints:List Intt:List Inta✝:DeletesZeroSumRuns s tih:t.sum = s.sum⊢ (a :: t).sum = (a :: s).sum simp [ih]All goals completed! 🐙
  | delete w s t hw _ ih =>deletes✝:List Intt✝:List Intw:List Ints:List Intt:List Inthw:w.sum = 0a✝:DeletesZeroSumRuns s tih:t.sum = s.sum⊢ t.sum = (w ++ s).sum simp [List.sum_append, hw, ih]All goals completed! 🐙

DeletesZeroSumRuns.prefix_sum says that after deleting runs that sum to zero, every prefix of the output has the sum of some prefix of the input. removeZeroSumSublists_noZeroRun uses it to show that a kept element can't start a run that sums to zero.

/-- Every prefix of the output has the sum of some prefix of the input. -/
theorem DeletesZeroSumRuns.prefix_sum
  {s t : List Int}
  (h : DeletesZeroSumRuns s t)
  : ∀ u, u <+: t → ∃ u', u' <+: s ∧ u.sum = u'.sum := bys:List Intt:List Inth:DeletesZeroSumRuns s t⊢ ∀ (u : List Int), u <+: t → ∃ u', u' <+: s ∧ u.sum = u'.sum
  induction h with
  | nil =>nils:List Intt:List Int⊢ ∀ (u : List Int), u <+: [] → ∃ u', u' <+: [] ∧ u.sum = u'.sum
    /- The only prefix of `[]` is `[]`. -/
    intro u hunils:List Intt:List Intu:List Inthu:u <+: []⊢ ∃ u', u' <+: [] ∧ u.sum = u'.sum
    rw [List.prefix_nilnils:List Intt:List Intu:List Inthu:u = []⊢ ∃ u', u' <+: [] ∧ u.sum = u'.sum] at hunils:List Intt:List Intu:List Inthu:u = []⊢ ∃ u', u' <+: [] ∧ u.sum = u'.sum
    exact ⟨[], List.nil_prefix, bys:List Intt:List Intu:List Inthu:u = []⊢ u.sum = [].sum simp [hu]All goals completed! 🐙⟩
  | keep a s t _ ih =>keeps✝:List Intt✝:List Inta:Ints:List Intt:List Inta✝:DeletesZeroSumRuns s tih:∀ (u : List Int), u <+: t → ∃ u', u' <+: s ∧ u.sum = u'.sum⊢ ∀ (u : List Int), u <+: a :: t → ∃ u', u' <+: a :: s ∧ u.sum = u'.sum
    /- A prefix of `a :: t` is `[]`, or `a` followed by a prefix of `t`. -/
    intro u hukeeps✝:List Intt✝:List Inta:Ints:List Intt:List Inta✝:DeletesZeroSumRuns s tih:∀ (u : List Int), u <+: t → ∃ u', u' <+: s ∧ u.sum = u'.sumu:List Inthu:u <+: a :: t⊢ ∃ u', u' <+: a :: s ∧ u.sum = u'.sum
    rcases List.prefix_cons_iff.mp hu with rfl | ⟨u₁, rfl, hu₁⟩keep.inls✝:List Intt✝:List Inta:Ints:List Intt:List Inta✝:DeletesZeroSumRuns s tih:∀ (u : List Int), u <+: t → ∃ u', u' <+: s ∧ u.sum = u'.sumhu:[] <+: a :: t⊢ ∃ u', u' <+: a :: s ∧ [].sum = u'.sumkeep.inrs✝:List Intt✝:List Inta:Ints:List Intt:List Inta✝:DeletesZeroSumRuns s tih:∀ (u : List Int), u <+: t → ∃ u', u' <+: s ∧ u.sum = u'.sumu₁:List Inthu₁:u₁ <+: thu:a :: u₁ <+: a :: t⊢ ∃ u', u' <+: a :: s ∧ (a :: u₁).sum = u'.sum
    ·keep.inls✝:List Intt✝:List Inta:Ints:List Intt:List Inta✝:DeletesZeroSumRuns s tih:∀ (u : List Int), u <+: t → ∃ u', u' <+: s ∧ u.sum = u'.sumhu:[] <+: a :: t⊢ ∃ u', u' <+: a :: s ∧ [].sum = u'.sum exact ⟨[], List.nil_prefix, rfl⟩All goals completed! 🐙
    ·keep.inrs✝:List Intt✝:List Inta:Ints:List Intt:List Inta✝:DeletesZeroSumRuns s tih:∀ (u : List Int), u <+: t → ∃ u', u' <+: s ∧ u.sum = u'.sumu₁:List Inthu₁:u₁ <+: thu:a :: u₁ <+: a :: t⊢ ∃ u', u' <+: a :: s ∧ (a :: u₁).sum = u'.sum obtain ⟨u', hu', hsum⟩ := ih u₁ hu₁keep.inrs✝:List Intt✝:List Inta:Ints:List Intt:List Inta✝:DeletesZeroSumRuns s tih:∀ (u : List Int), u <+: t → ∃ u', u' <+: s ∧ u.sum = u'.sumu₁:List Inthu₁:u₁ <+: thu:a :: u₁ <+: a :: tu':List Inthu':u' <+: shsum:u₁.sum = u'.sum⊢ ∃ u', u' <+: a :: s ∧ (a :: u₁).sum = u'.sum
      exact ⟨a :: u', List.cons_prefix_cons.mpr ⟨rfl, hu'⟩, bys✝:List Intt✝:List Inta:Ints:List Intt:List Inta✝:DeletesZeroSumRuns s tih:∀ (u : List Int), u <+: t → ∃ u', u' <+: s ∧ u.sum = u'.sumu₁:List Inthu₁:u₁ <+: thu:a :: u₁ <+: a :: tu':List Inthu':u' <+: shsum:u₁.sum = u'.sum⊢ (a :: u₁).sum = (a :: u').sum simp [hsum]All goals completed! 🐙⟩
  | delete w s t hw _ ih =>deletes✝:List Intt✝:List Intw:List Ints:List Intt:List Inthw:w.sum = 0a✝:DeletesZeroSumRuns s tih:∀ (u : List Int), u <+: t → ∃ u', u' <+: s ∧ u.sum = u'.sum⊢ ∀ (u : List Int), u <+: t → ∃ u', u' <+: w ++ s ∧ u.sum = u'.sum
    /- Put the deleted run `w` in front: it adds zero to the sum. -/
    intro u hudeletes✝:List Intt✝:List Intw:List Ints:List Intt:List Inthw:w.sum = 0a✝:DeletesZeroSumRuns s tih:∀ (u : List Int), u <+: t → ∃ u', u' <+: s ∧ u.sum = u'.sumu:List Inthu:u <+: t⊢ ∃ u', u' <+: w ++ s ∧ u.sum = u'.sum
    obtain ⟨u', hu', hsum⟩ := ih u hudeletes✝:List Intt✝:List Intw:List Ints:List Intt:List Inthw:w.sum = 0a✝:DeletesZeroSumRuns s tih:∀ (u : List Int), u <+: t → ∃ u', u' <+: s ∧ u.sum = u'.sumu:List Inthu:u <+: tu':List Inthu':u' <+: shsum:u.sum = u'.sum⊢ ∃ u', u' <+: w ++ s ∧ u.sum = u'.sum
    exact ⟨w ++ u', (List.prefix_append_right_inj w).mpr hu',
      bys✝:List Intt✝:List Intw:List Ints:List Intt:List Inthw:w.sum = 0a✝:DeletesZeroSumRuns s tih:∀ (u : List Int), u <+: t → ∃ u', u' <+: s ∧ u.sum = u'.sumu:List Inthu:u <+: tu':List Inthu':u' <+: shsum:u.sum = u'.sum⊢ u.sum = (w ++ u').sum simp [List.sum_append, hw, hsum]All goals completed! 🐙⟩

removeZeroSumSublists_deletes says that removeZeroSumSublists only deletes runs that sum to zero. Each case of the function is one case of DeletesZeroSumRuns, so the proof follows the function's recursion.

/-- `removeZeroSumSublists` deletes only runs that sum to zero. -/
theorem removeZeroSumSublists_deletes
  (s : List Int)
  : DeletesZeroSumRuns s (removeZeroSumSublists s) := bys:List Int⊢ DeletesZeroSumRuns s (removeZeroSumSublists s)
  /- Induction that follows the recursion of `removeZeroSumSublists`: each case
  of the function is one case of `DeletesZeroSumRuns`. -/
  fun_induction removeZeroSumSublists s with
  | case1 =>case1⊢ DeletesZeroSumRuns [] [] exact .nilAll goals completed! 🐙
  | case2 a rest j h ih =>case2a:Intrest:List Intj:Nath:List.findIdx? (fun x => x == 0) (List.scanl (fun x1 x2 => x1 + x2) a rest) = some jih:DeletesZeroSumRuns (List.drop j rest) (removeZeroSumSublists (List.drop j rest))⊢ DeletesZeroSumRuns (a :: rest) (removeZeroSumSublists (List.drop j rest))
    /- The `j`-th sum in the list is zero, and it is the sum of the first
    `j + 1` elements. -/
    obtain ⟨hj, hzero, _⟩ := List.findIdx?_eq_some_iff_getElem.mp hcase2a:Intrest:List Intj:Nath:List.findIdx? (fun x => x == 0) (List.scanl (fun x1 x2 => x1 + x2) a rest) = some jih:DeletesZeroSumRuns (List.drop j rest) (removeZeroSumSublists (List.drop j rest))hj:j < (List.scanl (fun x1 x2 => x1 + x2) a rest).lengthhzero:((List.scanl (fun x1 x2 => x1 + x2) a rest)[j] == 0) = trueright✝:∀ (j_1 : Nat) (hji : j_1 < j), ¬((List.scanl (fun x1 x2 => x1 + x2) a rest)[j_1] == 0) = true⊢ DeletesZeroSumRuns (a :: rest) (removeZeroSumSublists (List.drop j rest))
    have hsum : (a :: rest.take j).sum = 0 := bys:List Int⊢ DeletesZeroSumRuns s (removeZeroSumSublists s)
      rw [sum_cons_eq_foldl,a:Intrest:List Intj:Nath:List.findIdx? (fun x => x == 0) (List.scanl (fun x1 x2 => x1 + x2) a rest) = some jih:DeletesZeroSumRuns (List.drop j rest) (removeZeroSumSublists (List.drop j rest))hj:j < (List.scanl (fun x1 x2 => x1 + x2) a rest).lengthhzero:((List.scanl (fun x1 x2 => x1 + x2) a rest)[j] == 0) = trueright✝:∀ (j_1 : Nat) (hji : j_1 < j), ¬((List.scanl (fun x1 x2 => x1 + x2) a rest)[j_1] == 0) = true⊢ List.foldl (fun x1 x2 => x1 + x2) a (List.take j rest) = 0 ← List.getElem_scanl hja:Intrest:List Intj:Nath:List.findIdx? (fun x => x == 0) (List.scanl (fun x1 x2 => x1 + x2) a rest) = some jih:DeletesZeroSumRuns (List.drop j rest) (removeZeroSumSublists (List.drop j rest))hj:j < (List.scanl (fun x1 x2 => x1 + x2) a rest).lengthhzero:((List.scanl (fun x1 x2 => x1 + x2) a rest)[j] == 0) = trueright✝:∀ (j_1 : Nat) (hji : j_1 < j), ¬((List.scanl (fun x1 x2 => x1 + x2) a rest)[j_1] == 0) = true⊢ (List.scanl (fun x1 x2 => x1 + x2) a rest)[j] = 0]a:Intrest:List Intj:Nath:List.findIdx? (fun x => x == 0) (List.scanl (fun x1 x2 => x1 + x2) a rest) = some jih:DeletesZeroSumRuns (List.drop j rest) (removeZeroSumSublists (List.drop j rest))hj:j < (List.scanl (fun x1 x2 => x1 + x2) a rest).lengthhzero:((List.scanl (fun x1 x2 => x1 + x2) a rest)[j] == 0) = trueright✝:∀ (j_1 : Nat) (hji : j_1 < j), ¬((List.scanl (fun x1 x2 => x1 + x2) a rest)[j_1] == 0) = true⊢ (List.scanl (fun x1 x2 => x1 + x2) a rest)[j] = 0
      simpa using hzerocase2a:Intrest:List Intj:Nath:List.findIdx? (fun x => x == 0) (List.scanl (fun x1 x2 => x1 + x2) a rest) = some jih:DeletesZeroSumRuns (List.drop j rest) (removeZeroSumSublists (List.drop j rest))hj:j < (List.scanl (fun x1 x2 => x1 + x2) a rest).lengthhzero:((List.scanl (fun x1 x2 => x1 + x2) a rest)[j] == 0) = trueright✝:∀ (j_1 : Nat) (hji : j_1 < j), ¬((List.scanl (fun x1 x2 => x1 + x2) a rest)[j_1] == 0) = truehsum:(a :: List.take j rest).sum = 0⊢ DeletesZeroSumRuns (a :: rest) (removeZeroSumSublists (List.drop j rest))
    have e : a :: rest = (a :: rest.take j) ++ rest.drop j := bys:List Int⊢ DeletesZeroSumRuns s (removeZeroSumSublists s) simpcase2a:Intrest:List Intj:Nath:List.findIdx? (fun x => x == 0) (List.scanl (fun x1 x2 => x1 + x2) a rest) = some jih:DeletesZeroSumRuns (List.drop j rest) (removeZeroSumSublists (List.drop j rest))hj:j < (List.scanl (fun x1 x2 => x1 + x2) a rest).lengthhzero:((List.scanl (fun x1 x2 => x1 + x2) a rest)[j] == 0) = trueright✝:∀ (j_1 : Nat) (hji : j_1 < j), ¬((List.scanl (fun x1 x2 => x1 + x2) a rest)[j_1] == 0) = truehsum:(a :: List.take j rest).sum = 0e:a :: rest = a :: List.take j rest ++ List.drop j rest⊢ DeletesZeroSumRuns (a :: rest) (removeZeroSumSublists (List.drop j rest))
    rw [ecase2a:Intrest:List Intj:Nath:List.findIdx? (fun x => x == 0) (List.scanl (fun x1 x2 => x1 + x2) a rest) = some jih:DeletesZeroSumRuns (List.drop j rest) (removeZeroSumSublists (List.drop j rest))hj:j < (List.scanl (fun x1 x2 => x1 + x2) a rest).lengthhzero:((List.scanl (fun x1 x2 => x1 + x2) a rest)[j] == 0) = trueright✝:∀ (j_1 : Nat) (hji : j_1 < j), ¬((List.scanl (fun x1 x2 => x1 + x2) a rest)[j_1] == 0) = truehsum:(a :: List.take j rest).sum = 0e:a :: rest = a :: List.take j rest ++ List.drop j rest⊢ DeletesZeroSumRuns (a :: List.take j rest ++ List.drop j rest) (removeZeroSumSublists (List.drop j rest))]case2a:Intrest:List Intj:Nath:List.findIdx? (fun x => x == 0) (List.scanl (fun x1 x2 => x1 + x2) a rest) = some jih:DeletesZeroSumRuns (List.drop j rest) (removeZeroSumSublists (List.drop j rest))hj:j < (List.scanl (fun x1 x2 => x1 + x2) a rest).lengthhzero:((List.scanl (fun x1 x2 => x1 + x2) a rest)[j] == 0) = trueright✝:∀ (j_1 : Nat) (hji : j_1 < j), ¬((List.scanl (fun x1 x2 => x1 + x2) a rest)[j_1] == 0) = truehsum:(a :: List.take j rest).sum = 0e:a :: rest = a :: List.take j rest ++ List.drop j rest⊢ DeletesZeroSumRuns (a :: List.take j rest ++ List.drop j rest) (removeZeroSumSublists (List.drop j rest))
    exact .delete _ _ _ hsum ihAll goals completed! 🐙
  | case3 a rest h ih =>case3a:Intrest:List Inth:List.findIdx? (fun x => x == 0) (List.scanl (fun x1 x2 => x1 + x2) a rest) = noneih:DeletesZeroSumRuns rest (removeZeroSumSublists rest)⊢ DeletesZeroSumRuns (a :: rest) (a :: removeZeroSumSublists rest) exact .keep a _ _ ihAll goals completed! 🐙

removeZeroSumSublists_noZeroRun says that no run of the output, other than [], sums to zero. A run that starts with a kept element a has the sum of a nonempty prefix of a :: rest, and the function keeps a only when none of those sums to zero.

/-- No run of the output of `removeZeroSumSublists`, other than `[]`, sums to
zero. -/
theorem removeZeroSumSublists_noZeroRun
  (s : List Int)
  : ∀ w, w <:+: removeZeroSumSublists s → w ≠ [] → w.sum ≠ 0 := bys:List Int⊢ ∀ (w : List Int), w <:+: removeZeroSumSublists s → w ≠ [] → w.sum ≠ 0
  /- Induction that follows the recursion of `removeZeroSumSublists`. -/
  fun_induction removeZeroSumSublists s with
  | case1 =>case1⊢ ∀ (w : List Int), w <:+: [] → w ≠ [] → w.sum ≠ 0
    /- The only run of `[]` is `[]`. -/
    intro w hw hnecase1w:List Inthw:w <:+: []hne:w ≠ []⊢ w.sum ≠ 0
    simp_allAll goals completed! 🐙
  | case2 a rest j h ih =>case2a:Intrest:List Intj:Nath:List.findIdx? (fun x => x == 0) (List.scanl (fun x1 x2 => x1 + x2) a rest) = some jih:∀ (w : List Int), w <:+: removeZeroSumSublists (List.drop j rest) → w ≠ [] → w.sum ≠ 0⊢ ∀ (w : List Int), w <:+: removeZeroSumSublists (List.drop j rest) → w ≠ [] → w.sum ≠ 0 exact ihAll goals completed! 🐙
  | case3 a rest h ih =>case3a:Intrest:List Inth:List.findIdx? (fun x => x == 0) (List.scanl (fun x1 x2 => x1 + x2) a rest) = noneih:∀ (w : List Int), w <:+: removeZeroSumSublists rest → w ≠ [] → w.sum ≠ 0⊢ ∀ (w : List Int), w <:+: a :: removeZeroSumSublists rest → w ≠ [] → w.sum ≠ 0
    /- A run of `a :: t` is a prefix of `a :: t`, or a run of `t`. -/
    intro w hw hnecase3a:Intrest:List Inth:List.findIdx? (fun x => x == 0) (List.scanl (fun x1 x2 => x1 + x2) a rest) = noneih:∀ (w : List Int), w <:+: removeZeroSumSublists rest → w ≠ [] → w.sum ≠ 0w:List Inthw:w <:+: a :: removeZeroSumSublists resthne:w ≠ []⊢ w.sum ≠ 0
    rcases List.infix_cons_iff.mp hw with hp | hicase3.inla:Intrest:List Inth:List.findIdx? (fun x => x == 0) (List.scanl (fun x1 x2 => x1 + x2) a rest) = noneih:∀ (w : List Int), w <:+: removeZeroSumSublists rest → w ≠ [] → w.sum ≠ 0w:List Inthw:w <:+: a :: removeZeroSumSublists resthne:w ≠ []hp:w <+: a :: removeZeroSumSublists rest⊢ w.sum ≠ 0case3.inra:Intrest:List Inth:List.findIdx? (fun x => x == 0) (List.scanl (fun x1 x2 => x1 + x2) a rest) = noneih:∀ (w : List Int), w <:+: removeZeroSumSublists rest → w ≠ [] → w.sum ≠ 0w:List Inthw:w <:+: a :: removeZeroSumSublists resthne:w ≠ []hi:w <:+: removeZeroSumSublists rest⊢ w.sum ≠ 0
    ·case3.inla:Intrest:List Inth:List.findIdx? (fun x => x == 0) (List.scanl (fun x1 x2 => x1 + x2) a rest) = noneih:∀ (w : List Int), w <:+: removeZeroSumSublists rest → w ≠ [] → w.sum ≠ 0w:List Inthw:w <:+: a :: removeZeroSumSublists resthne:w ≠ []hp:w <+: a :: removeZeroSumSublists rest⊢ w.sum ≠ 0 rcases List.prefix_cons_iff.mp hp with rfl | ⟨w₁, rfl, hw₁⟩case3.inl.inla:Intrest:List Inth:List.findIdx? (fun x => x == 0) (List.scanl (fun x1 x2 => x1 + x2) a rest) = noneih:∀ (w : List Int), w <:+: removeZeroSumSublists rest → w ≠ [] → w.sum ≠ 0hw:[] <:+: a :: removeZeroSumSublists resthne:[] ≠ []hp:[] <+: a :: removeZeroSumSublists rest⊢ [].sum ≠ 0case3.inl.inra:Intrest:List Inth:List.findIdx? (fun x => x == 0) (List.scanl (fun x1 x2 => x1 + x2) a rest) = noneih:∀ (w : List Int), w <:+: removeZeroSumSublists rest → w ≠ [] → w.sum ≠ 0w₁:List Inthw₁:w₁ <+: removeZeroSumSublists resthw:a :: w₁ <:+: a :: removeZeroSumSublists resthne:a :: w₁ ≠ []hp:a :: w₁ <+: a :: removeZeroSumSublists rest⊢ (a :: w₁).sum ≠ 0
      ·case3.inl.inla:Intrest:List Inth:List.findIdx? (fun x => x == 0) (List.scanl (fun x1 x2 => x1 + x2) a rest) = noneih:∀ (w : List Int), w <:+: removeZeroSumSublists rest → w ≠ [] → w.sum ≠ 0hw:[] <:+: a :: removeZeroSumSublists resthne:[] ≠ []hp:[] <+: a :: removeZeroSumSublists rest⊢ [].sum ≠ 0 exact absurd rfl hneAll goals completed! 🐙
      ·case3.inl.inra:Intrest:List Inth:List.findIdx? (fun x => x == 0) (List.scanl (fun x1 x2 => x1 + x2) a rest) = noneih:∀ (w : List Int), w <:+: removeZeroSumSublists rest → w ≠ [] → w.sum ≠ 0w₁:List Inthw₁:w₁ <+: removeZeroSumSublists resthw:a :: w₁ <:+: a :: removeZeroSumSublists resthne:a :: w₁ ≠ []hp:a :: w₁ <+: a :: removeZeroSumSublists rest⊢ (a :: w₁).sum ≠ 0 /- `w` is `a :: w₁`, and `w₁` has the sum of a prefix `u'` of
        `rest`. So `w` has the sum of `a :: u'`, a nonempty prefix of
        `a :: rest`, and none of those sums to zero. -/
        obtain ⟨u', hu', hsum⟩ :=
          (removeZeroSumSublists_deletes rest).prefix_sum w₁ hw₁case3.inl.inra:Intrest:List Inth:List.findIdx? (fun x => x == 0) (List.scanl (fun x1 x2 => x1 + x2) a rest) = noneih:∀ (w : List Int), w <:+: removeZeroSumSublists rest → w ≠ [] → w.sum ≠ 0w₁:List Inthw₁:w₁ <+: removeZeroSumSublists resthw:a :: w₁ <:+: a :: removeZeroSumSublists resthne:a :: w₁ ≠ []hp:a :: w₁ <+: a :: removeZeroSumSublists restu':List Inthu':u' <+: resthsum:w₁.sum = u'.sum⊢ (a :: w₁).sum ≠ 0
        have hlen : u'.length < (rest.scanl (· + ·) a).length := bys:List Int⊢ ∀ (w : List Int), w <:+: removeZeroSumSublists s → w ≠ [] → w.sum ≠ 0
          have := hu'.length_lea:Intrest:List Inth:List.findIdx? (fun x => x == 0) (List.scanl (fun x1 x2 => x1 + x2) a rest) = noneih:∀ (w : List Int), w <:+: removeZeroSumSublists rest → w ≠ [] → w.sum ≠ 0w₁:List Inthw₁:w₁ <+: removeZeroSumSublists resthw:a :: w₁ <:+: a :: removeZeroSumSublists resthne:a :: w₁ ≠ []hp:a :: w₁ <+: a :: removeZeroSumSublists restu':List Inthu':u' <+: resthsum:w₁.sum = u'.sumthis:u'.length ≤ rest.length⊢ u'.length < (List.scanl (fun x1 x2 => x1 + x2) a rest).length
          simpa:Intrest:List Inth:List.findIdx? (fun x => x == 0) (List.scanl (fun x1 x2 => x1 + x2) a rest) = noneih:∀ (w : List Int), w <:+: removeZeroSumSublists rest → w ≠ [] → w.sum ≠ 0w₁:List Inthw₁:w₁ <+: removeZeroSumSublists resthw:a :: w₁ <:+: a :: removeZeroSumSublists resthne:a :: w₁ ≠ []hp:a :: w₁ <+: a :: removeZeroSumSublists restu':List Inthu':u' <+: resthsum:w₁.sum = u'.sumthis:u'.length ≤ rest.length⊢ u'.length < rest.length + 1
          omegacase3.inl.inra:Intrest:List Inth:List.findIdx? (fun x => x == 0) (List.scanl (fun x1 x2 => x1 + x2) a rest) = noneih:∀ (w : List Int), w <:+: removeZeroSumSublists rest → w ≠ [] → w.sum ≠ 0w₁:List Inthw₁:w₁ <+: removeZeroSumSublists resthw:a :: w₁ <:+: a :: removeZeroSumSublists resthne:a :: w₁ ≠ []hp:a :: w₁ <+: a :: removeZeroSumSublists restu':List Inthu':u' <+: resthsum:w₁.sum = u'.sumhlen:u'.length < (List.scanl (fun x1 x2 => x1 + x2) a rest).length⊢ (a :: w₁).sum ≠ 0
        have hmem := List.getElem_mem hlencase3.inl.inra:Intrest:List Inth:List.findIdx? (fun x => x == 0) (List.scanl (fun x1 x2 => x1 + x2) a rest) = noneih:∀ (w : List Int), w <:+: removeZeroSumSublists rest → w ≠ [] → w.sum ≠ 0w₁:List Inthw₁:w₁ <+: removeZeroSumSublists resthw:a :: w₁ <:+: a :: removeZeroSumSublists resthne:a :: w₁ ≠ []hp:a :: w₁ <+: a :: removeZeroSumSublists restu':List Inthu':u' <+: resthsum:w₁.sum = u'.sumhlen:u'.length < (List.scanl (fun x1 x2 => x1 + x2) a rest).lengthhmem:(List.scanl (fun x1 x2 => x1 + x2) a rest)[u'.length] ∈ List.scanl (fun x1 x2 => x1 + x2) a rest⊢ (a :: w₁).sum ≠ 0
        rw [List.getElem_scanl,case3.inl.inra:Intrest:List Inth:List.findIdx? (fun x => x == 0) (List.scanl (fun x1 x2 => x1 + x2) a rest) = noneih:∀ (w : List Int), w <:+: removeZeroSumSublists rest → w ≠ [] → w.sum ≠ 0w₁:List Inthw₁:w₁ <+: removeZeroSumSublists resthw:a :: w₁ <:+: a :: removeZeroSumSublists resthne:a :: w₁ ≠ []hp:a :: w₁ <+: a :: removeZeroSumSublists restu':List Inthu':u' <+: resthsum:w₁.sum = u'.sumhlen:u'.length < (List.scanl (fun x1 x2 => x1 + x2) a rest).lengthhmem:List.foldl (fun x1 x2 => x1 + x2) a (List.take u'.length rest) ∈ List.scanl (fun x1 x2 => x1 + x2) a rest⊢ (a :: w₁).sum ≠ 0 ← List.prefix_iff_eq_take.mp hu',case3.inl.inra:Intrest:List Inth:List.findIdx? (fun x => x == 0) (List.scanl (fun x1 x2 => x1 + x2) a rest) = noneih:∀ (w : List Int), w <:+: removeZeroSumSublists rest → w ≠ [] → w.sum ≠ 0w₁:List Inthw₁:w₁ <+: removeZeroSumSublists resthw:a :: w₁ <:+: a :: removeZeroSumSublists resthne:a :: w₁ ≠ []hp:a :: w₁ <+: a :: removeZeroSumSublists restu':List Inthu':u' <+: resthsum:w₁.sum = u'.sumhlen:u'.length < (List.scanl (fun x1 x2 => x1 + x2) a rest).lengthhmem:List.foldl (fun x1 x2 => x1 + x2) a u' ∈ List.scanl (fun x1 x2 => x1 + x2) a rest⊢ (a :: w₁).sum ≠ 0
          ← sum_cons_eq_foldlcase3.inl.inra:Intrest:List Inth:List.findIdx? (fun x => x == 0) (List.scanl (fun x1 x2 => x1 + x2) a rest) = noneih:∀ (w : List Int), w <:+: removeZeroSumSublists rest → w ≠ [] → w.sum ≠ 0w₁:List Inthw₁:w₁ <+: removeZeroSumSublists resthw:a :: w₁ <:+: a :: removeZeroSumSublists resthne:a :: w₁ ≠ []hp:a :: w₁ <+: a :: removeZeroSumSublists restu':List Inthu':u' <+: resthsum:w₁.sum = u'.sumhlen:u'.length < (List.scanl (fun x1 x2 => x1 + x2) a rest).lengthhmem:(a :: u').sum ∈ List.scanl (fun x1 x2 => x1 + x2) a rest⊢ (a :: w₁).sum ≠ 0] at hmemcase3.inl.inra:Intrest:List Inth:List.findIdx? (fun x => x == 0) (List.scanl (fun x1 x2 => x1 + x2) a rest) = noneih:∀ (w : List Int), w <:+: removeZeroSumSublists rest → w ≠ [] → w.sum ≠ 0w₁:List Inthw₁:w₁ <+: removeZeroSumSublists resthw:a :: w₁ <:+: a :: removeZeroSumSublists resthne:a :: w₁ ≠ []hp:a :: w₁ <+: a :: removeZeroSumSublists restu':List Inthu':u' <+: resthsum:w₁.sum = u'.sumhlen:u'.length < (List.scanl (fun x1 x2 => x1 + x2) a rest).lengthhmem:(a :: u').sum ∈ List.scanl (fun x1 x2 => x1 + x2) a rest⊢ (a :: w₁).sum ≠ 0
        have hne0 := List.findIdx?_eq_none_iff.mp h _ hmemcase3.inl.inra:Intrest:List Inth:List.findIdx? (fun x => x == 0) (List.scanl (fun x1 x2 => x1 + x2) a rest) = noneih:∀ (w : List Int), w <:+: removeZeroSumSublists rest → w ≠ [] → w.sum ≠ 0w₁:List Inthw₁:w₁ <+: removeZeroSumSublists resthw:a :: w₁ <:+: a :: removeZeroSumSublists resthne:a :: w₁ ≠ []hp:a :: w₁ <+: a :: removeZeroSumSublists restu':List Inthu':u' <+: resthsum:w₁.sum = u'.sumhlen:u'.length < (List.scanl (fun x1 x2 => x1 + x2) a rest).lengthhmem:(a :: u').sum ∈ List.scanl (fun x1 x2 => x1 + x2) a resthne0:((a :: u').sum == 0) = false⊢ (a :: w₁).sum ≠ 0
        simp at hne0case3.inl.inra:Intrest:List Inth:List.findIdx? (fun x => x == 0) (List.scanl (fun x1 x2 => x1 + x2) a rest) = noneih:∀ (w : List Int), w <:+: removeZeroSumSublists rest → w ≠ [] → w.sum ≠ 0w₁:List Inthw₁:w₁ <+: removeZeroSumSublists resthw:a :: w₁ <:+: a :: removeZeroSumSublists resthne:a :: w₁ ≠ []hp:a :: w₁ <+: a :: removeZeroSumSublists restu':List Inthu':u' <+: resthsum:w₁.sum = u'.sumhlen:u'.length < (List.scanl (fun x1 x2 => x1 + x2) a rest).lengthhmem:(a :: u').sum ∈ List.scanl (fun x1 x2 => x1 + x2) a resthne0:¬a + u'.sum = 0⊢ (a :: w₁).sum ≠ 0
        simpa [hsum] using hne0All goals completed! 🐙
    ·case3.inra:Intrest:List Inth:List.findIdx? (fun x => x == 0) (List.scanl (fun x1 x2 => x1 + x2) a rest) = noneih:∀ (w : List Int), w <:+: removeZeroSumSublists rest → w ≠ [] → w.sum ≠ 0w:List Inthw:w <:+: a :: removeZeroSumSublists resthne:w ≠ []hi:w <:+: removeZeroSumSublists rest⊢ w.sum ≠ 0 exact ih w hi hneAll goals completed! 🐙

The Goal

We need a proof for the proposition SolvesLeetCode1171 removeZeroSumSublists. That would prove that removeZeroSumSublists meets the specification on every input.

The following proof combines the lemmas above.

/-- `removeZeroSumSublists` meets the specification of LeetCode 1171. -/
example
  : SolvesLeetCode1171 removeZeroSumSublists := by⊢ SolvesLeetCode1171 removeZeroSumSublists
  intro ss:List Int⊢ RemoveZeroSumSpec s (removeZeroSumSublists s)
  /- Deleting runs that sum to zero keeps the sum. -/
  have hd := removeZeroSumSublists_deletes ss:List Inthd:DeletesZeroSumRuns s (removeZeroSumSublists s)⊢ RemoveZeroSumSpec s (removeZeroSumSublists s)
  exact ⟨hd.sum_eq, hd, removeZeroSumSublists_noZeroRun s⟩All goals completed! 🐙

That's the whole exercise: a specification, a solution, and a proof that the solution meets the specification, all checked by Lean. The hardest part was not the proof but the specification.

Thanks for reading!