ExampleConstruction: AI-adaptedVerification: AI-generatedprecheck passverified 2026-08-02 (claude-opus-5)

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

Pascal's triangle computed to row $6$ , with Pascal's rule checked at every interior entry

Example

The array whose $n$ -th row is $(\binom{n}{0}), (\binom{n}{1}), \dots, (\binom{n}{n})$ is Pascal's triangle. Rows $0$ to $6$ are

$\begin{array}{c} 1 \\ 1 1 \\ 1 2 1 \\ 1 3 3 1 \\ 1 4 6 4 1 \\ 1 5 10 10 5 1 \\ 1 6 15 20 15 6 1 \end{array}$

Every interior entry is produced below by Pascal's rule $(\binom{n + 1}{k + 1}) = (\binom{n}{k}) + (\binom{n}{k + 1})$ , and the hockey-stick identity $\sum_{i \leq n} (\binom{i}{k}) = (\binom{n + 1}{k + 1})$ from the row above, the boundary entries being the values $(\binom{n}{0}) = (\binom{n}{n}) = 1$ ; four interior entries are cross-checked against the closed formula of $(\binom{n}{k}) k! (n - k)! = n!$ for $k \leq n$ ; hence $(\binom{n}{k}) k! = n^{\underline{k}}$ , the quotient $n! / (k! (n - k)!)$ is a natural number, and $(\binom{n}{k}) = (\binom{n}{n - k})$ . The row sums and the alternating row sums are then checked against $\sum_{k < n + 1} (\binom{n}{k}) = 2^{n}$ , and $\sum_{k < n + 1} (- 1)^{k} ι ⁣ (\binom{n}{k}) = 0$ for $n \geq 1$ , including the row where the alternating sum is not zero.

Facts & Assumptions

Given: The binomial coefficients of The set $[A]^{k}$ of $k$ -element subsets and the binomial coefficient $(\binom{n}{k}) : = ∣ [n]^{k} ∣$ and the factorials $0! = 1$ , $1! = 1$ , $2! = 2$ , $3! = 6$ , $4! = 24$ , $5! = 120$ , $6! = 720$ of The factorial $n!$ and the falling factorial $n^{\underline{k}}$ , defined by recursion in $N$ .

[L1]

Boundary values: $(\binom{n}{0}) = (\binom{n}{n}) = 1$ for every $n$ , and $(\binom{n}{k}) = 0$ for $k > n$ (The set $[A]^{k}$ of $k$ -element subsets and the binomial coefficient $(\binom{n}{k}) : = ∣ [n]^{k} ∣$ ).

[L2]

Pascal's rule: $(\binom{n + 1}{k + 1}) = (\binom{n}{k}) + (\binom{n}{k + 1})$ (Pascal's rule $(\binom{n + 1}{k + 1}) = (\binom{n}{k}) + (\binom{n}{k + 1})$ , and the hockey-stick identity $\sum_{i \leq n} (\binom{i}{k}) = (\binom{n + 1}{k + 1})$ ).

[L3]

The closed formula: $(\binom{n}{k}) k! (n - k)! = n!$ for $k \leq n$ , so $(\binom{n}{k})$ is the natural number whose canonical natural is $ι (n!) / (ι (k!) ι ((n - k)!))$ ( $(\binom{n}{k}) k! (n - k)! = n!$ for $k \leq n$ ; hence $(\binom{n}{k}) k! = n^{\underline{k}}$ , the quotient $n! / (k! (n - k)!)$ is a natural number, and $(\binom{n}{k}) = (\binom{n}{n - k})$ , The canonical natural $ι (n) = n \cdot 1_{F}$ of a field).

[L4]

Row sums: $\sum_{k < n + 1} (\binom{n}{k}) = 2^{n}$ , and $\sum_{k < n + 1} (- 1)^{k} ι (\binom{n}{k}) = 0$ for $n \geq 1$ ( $\sum_{k < n + 1} (\binom{n}{k}) = 2^{n}$ , and $\sum_{k < n + 1} (- 1)^{k} ι ⁣ (\binom{n}{k}) = 0$ for $n \geq 1$ , Exponentiation of natural numbers, $m^{n}$ , and its agreement with the integer power in $R$ , Finite sums and finite products of natural numbers, $\sum_{k < n} a_{k}$ and $\prod_{k < n} a_{k}$ in $N$ ).

Verification

technique · direct

1.1

Row $0$ is the single entry $(\binom{0}{0}) = 1$ , and row $1$ is $(\binom{1}{0}) = 1$ , $(\binom{1}{1}) = 1$ , both by [L1]. Every row begins and ends with $1$ for the same reason.

givenL1

2.1

The interior entries, each by [L2] from the row above. Row $2$ : $(\binom{2}{1}) = (\binom{1}{0}) + (\binom{1}{1}) = 2$ . Row $3$ : $(\binom{3}{1}) = (\binom{2}{0}) + (\binom{2}{1}) = 3$ and $(\binom{3}{2}) = (\binom{2}{1}) + (\binom{2}{2}) = 3$ . Row $4$ : $4$ , $(\binom{4}{2}) = 3 + 3 = 6$ , $4$ . Row $5$ : $5$ , $(\binom{5}{2}) = 4 + 6 = 10$ , $(\binom{5}{3}) = 6 + 4 = 10$ , $5$ . Row $6$ : $6$ , $(\binom{6}{2}) = 5 + 10 = 15$ , $(\binom{6}{3}) = 10 + 10 = 20$ , $(\binom{6}{4}) = 10 + 5 = 15$ , $6$ . This is the array displayed above.

step 1.1L1L2

3.1

The closed formula agrees, checked on four interior entries by [L3]: $(\binom{4}{2}) \cdot 2! \cdot 2! = 6 \cdot 2 \cdot 2 = 24 = 4!$ ; $(\binom{5}{2}) \cdot 2! \cdot 3! = 10 \cdot 2 \cdot 6 = 120 = 5!$ ; $(\binom{6}{2}) \cdot 2! \cdot 4! = 15 \cdot 2 \cdot 24 = 720 = 6!$ ; $(\binom{6}{3}) \cdot 3! \cdot 3! = 20 \cdot 6 \cdot 6 = 720 = 6!$ . So the two routes give the same numbers.

step 2.1L3

3.2

The row sums are $1$ , $1 + 1 = 2$ , $1 + 2 + 1 = 4$ , $1 + 3 + 3 + 1 = 8$ , $1 + 4 + 6 + 4 + 1 = 16$ , $1 + 5 + 10 + 10 + 5 + 1 = 32$ and $1 + 6 + 15 + 20 + 15 + 6 + 1 = 64$ , that is $2^{0}, 2^{1}, \dots, 2^{6}$ , as [L4] requires.

step 2.1L4

3.3

The alternating row sums are $1$ for row $0$ , and $1 - 1 = 0$ , $1 - 2 + 1 = 0$ , $1 - 3 + 3 - 1 = 0$ , $1 - 4 + 6 - 4 + 1 = 0$ , $1 - 5 + 10 - 10 + 5 - 1 = 0$ , $1 - 6 + 15 - 20 + 15 - 6 + 1 = 0$ for rows $1$ to $6$ . Row $0$ is the exception, and it is exactly the row where the hypothesis $n \geq 1$ of [L4] fails: the sum there has the single term $(\binom{0}{0}) = 1$ .

step 2.1L1L4

4.1

Rows $0$ to $6$ are as displayed, each interior entry agreeing with [L2] and the four checked in step 3.1 agreeing with [L3], the row sums with the powers of $2$ , and the alternating sums with $0$ from row $1$ onwards and with $1$ at row $0$ .

step 3.1step 3.2step 3.3∎

Remarks

The exceptional row is the point of the last check. A reader who computes only rows $1$ to $6$ sees an alternating sum that is always $0$ and will state the identity for every $n$ . Row $0$ is where that statement is false, and this page records it as a false statement for exactly that reason (FALSE: $\sum_{k < n + 1} (- 1)^{k} ι ⁣ (\binom{n}{k}) = 0$ for every $n \in N$ ).
Symmetry is visible in every row and is $(\binom{n}{k}) k! (n - k)! = n!$ for $k \leq n$ ; hence $(\binom{n}{k}) k! = n^{\underline{k}}$ , the quotient $n! / (k! (n - k)!)$ is a natural number, and $(\binom{n}{k}) = (\binom{n}{n - k})$ clause 3: row $6$ read backwards is row $6$ .

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

42 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

Pascal's triangle (Wikipedia) (standard reference, not scraped)
Pascal's rule (Wikipedia) (standard reference, not scraped)
Binomial coefficient (Wikipedia) (standard reference, not scraped)

Pascal's triangle computed to row 66, with Pascal's rule checked at every interior entry