Probability · medium

Statement, exactly as the model and Lean see it

theorem lg_target (n : ℕ) : ∑ k ∈ Finset.range (n + 1), Nat.choose n k = 2 ^ n := by

Source: Written for LeanGraph, reference proof certified
Premises used by the reference proof: 1

Traces

Each configuration's full record: what was retrieved, what the model wrote, what Lean said back.

Verified3 model calls · 3 Lean checks · $0.00050

Retrieved lemmas

1. Nat.sum_range_choose
2. Nat.sum_range_mul_choose
3. Int.alternating_sum_range_choose_eq_choose
4. Nat.sum_range_choose_sq
5. Nat.sum_range_multichoose
6. bernoulli'_def
7. sum_bernoulli'
8. sum_bernoulli

Plan

### Explanation of the Proof: The theorem `lg_target` states that the sum of binomial coefficients $\sum_{k=0}^{n} \binom{n}{k} = 2^n$. This is a well-known identity in combinatorics, which can be understood as follows: each binomial coefficient $\binom{n}{k}$ counts the number of ways to choose $k$ elements from a set of size $n$, and the total over all $k$ gives the total number of subsets of a set of size $n$, which is $2^n$. Among the provided lemmas, the most relevant one is: - `Nat.sum_range_choose (n : ℕ) : ∑ m ∈ Finset.range (n + 1), n.choose m = 2 ^ n` This lemma directly expresses the identity we want to prove. Therefore, the proof is essentially a matter of applying this lemma with the correct parameters. --- ### Lean Proof Skeleton: This proof uses the `rw` tactic to rewrite the goal using the known lemma `Nat.sum_range_choose`, thereby completing the proof in one step.

Skeleton — Lean reported problems

import Mathlib.Data.Nat.Basic
import Mathlib.Data.Finset.Basic

theorem lg_target (n : ℕ) : ∑ k ∈ Finset.range (n + 1), Nat.choose n k = 2 ^ n := by
  -- The lemma directly provides the result
  rw [Nat.sum_range_choose n]

Attempts

sample 0 · round 0Forbidden token2.3 s model time

Proof

import Mathlib.Data.Nat.Basic
import Mathlib.Data.Finset.Basic

theorem lg_target (n : ℕ) : ∑ k ∈ Finset.range (n + 1), Nat.choose n k = 2 ^ n := by
  rw [Nat.sum_range_choose n]

What Lean printed (this is all the model sees on repair)

rejected before compilation: forbidden token(s): command

sample 0 · round 1Verified1.9 s model time
Proof
```
rw [Nat.sum_range_choose n]
```

Verified proof

theorem lg_target (n : ℕ) : ∑ k ∈ Finset.range (n + 1), Nat.choose n k = 2 ^ n := by
  rw [Nat.sum_range_choose n]

Axioms used: propext, Classical.choice, Quot.sound

Reference proof

The proof we wrote and certified before any model ran.

exact Nat.sum_range_choose n