ExampleConstruction: AI-generatedVerification: AI-generatedSession-authored (Fable 5 assisted)precheck passjudge pass (z-ai/glm-5.2)audited 2026-07-29

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.

Vandermonde's identity checked at $m = 4$ , $n = 3$ , $k = 3$ , both sides equal to $35$

Example

Take $m = 4$ , $n = 3$ and $k = 3$ in Vandermonde's identity $\binom{m+n}{k} = \sum_{i<k+1}\binom{m}{i}\binom{n}{k-i}$ . The left-hand side is $\binom{7}{3} = 35$ , and the right-hand side is

$\binom{4}{0}\binom{3}{3} + \binom{4}{1}\binom{3}{2} + \binom{4}{2}\binom{3}{1} + \binom{4}{3}\binom{3}{0} = 1 + 12 + 18 + 4 = 35 .$

The same identity at $k = 5$ , still with $m = 4$ and $n = 3$ , exercises the boundary convention: three of the six terms vanish because their coefficients are $0$ , and both sides come to $21$ .

Facts & Assumptions

Given: $M := 4\times\{0\}$ and $N := 3\times\{1\}$ , disjoint with $\lvert M\rvert = 4$ , $\lvert N\rvert = 3$ and $\lvert M\cup N\rvert = 7$ ; and the factorials $2! = 2$ , $3! = 6$ , $4! = 24$ , $5! = 120$ , $7! = 5040$ (The factorial $n!$ and the falling factorial $n^{\underline{k}}$ , defined by recursion in $\mathbb{N}$ ).

[L1]

Vandermonde: $\binom{m+n}{k} = \sum_{i<k+1}\binom{m}{i}\binom{n}{k-i}$ , proved by partitioning $[M\cup N]^{k}$ according to $\lvert S \cap M\rvert$ , the block with value $i$ being in bijection with $[M]^{i}\times[N]^{k-i}$ (Vandermonde's identity $\binom{m+n}{k} = \sum_{i<k+1}\binom{m}{i}\binom{n}{k-i}$ , The sum rule: a finite disjoint union is finite with $\lvert A \cup B\rvert = \lvert A\rvert + \lvert B\rvert$ and $\lvert\bigcup_{i \in I} A_i\rvert = \sum_{i \in I}\lvert A_i\rvert$ , and a sum over a finite index set splits along a partition, The product rule: $\lvert A \times B\rvert = \lvert A\rvert\,\lvert B\rvert$ , and $\big\lvert\prod_{i<m} A_i\big\rvert = \prod_{i<m}\lvert A_i\rvert$ ).

[L2]

$\binom{n}{k}k!(n-k)! = n!$ for $k \le n$ ( $\binom{n}{k}\,k!\,(n-k)! = n!$ for $k \le 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}$ ), cancellation by a nonzero natural (Cancellation for multiplication by a nonzero factor), and $\binom{n}{0} = \binom{n}{n} = 1$ , $\binom{n}{1} = n$ , $\binom{n}{k} = 0$ for $k>n$ (The set $[A]^{k}$ of $k$ -element subsets and the binomial coefficient $\binom{n}{k} := \lvert [n]^{k}\rvert$ ).

[L3]

Finite sums in $\mathbb{N}$ (Finite sums and finite products of natural numbers, $\sum_{k<n} a_k$ and $\prod_{k<n} a_k$ in $\mathbb{N}$ ).

Verification

technique · direct

1.1

The coefficients needed, all from [L2]. $\binom{7}{3}\cdot 3!\cdot 4! = 7!$ gives $\binom{7}{3}\cdot 6\cdot 24 = 5040$ , so $\binom{7}{3}\cdot 144 = 5040$ and $\binom{7}{3} = 35$ . Similarly $\binom{4}{2}\cdot 2!\cdot 2! = 4!$ gives $\binom{4}{2} = 6$ ; and $\binom{4}{0} = \binom{3}{3} = \binom{3}{0} = 1$ , $\binom{4}{1} = 4$ , $\binom{4}{3} = \binom{4}{1} = 4$ by symmetry, $\binom{3}{1} = \binom{3}{2} = 3$ . Also $\binom{7}{5}\cdot 5!\cdot 2! = 7!$ gives $\binom{7}{5}\cdot 240 = 5040$ , so $\binom{7}{5} = 21$ .

givenL2

2.1

The case $k = 3$ . The four terms of the sum, indexed by $i < 4$ , are $\binom{4}{0}\binom{3}{3} = 1\cdot 1 = 1$ , $\binom{4}{1}\binom{3}{2} = 4\cdot 3 = 12$ , $\binom{4}{2}\binom{3}{1} = 6\cdot 3 = 18$ and $\binom{4}{3}\binom{3}{0} = 4\cdot 1 = 4$ ; their sum is $1+12+18+4 = 35$ , equal to $\binom{7}{3}$ .

step 1.1L1L3

2.2

The case $k = 5$ , where the boundary convention does the work. The sum runs over $i < 6$ and its terms are $\binom{4}{0}\binom{3}{5} = 0$ , $\binom{4}{1}\binom{3}{4} = 0$ , $\binom{4}{2}\binom{3}{3} = 6$ , $\binom{4}{3}\binom{3}{2} = 12$ , $\binom{4}{4}\binom{3}{1} = 3$ and $\binom{4}{5}\binom{3}{0} = 0$ , the vanishing ones being those with $5-i > 3$ or $i > 4$ . The total is $6+12+3 = 21 = \binom{7}{5}$ .

step 1.1L1L2L3

3.1

The partition behind one block. The term with $i = 2$ in step 2.1 counts the sets $S \in [M\cup N]^{3}$ with exactly two elements in $M$ ; the bijection of [L1] sends such an $S$ to the pair $(S\cap M, S\cap N)$ . For instance $S = \{(0,0),(1,0),(0,1)\}$ goes to $\big(\{(0,0),(1,0)\},\ \{(0,1)\}\big) \in [M]^{2}\times[N]^{1}$ , and there are $\binom{4}{2}\binom{3}{1} = 18$ such $S$ , which is the value computed there. So the identity is a count, not an algebraic accident.

step 1.1step 2.1L1

4.1

Both instances confirm [L1]: at $k = 3$ both sides are $35$ , at $k = 5$ both sides are $21$ , and in the second the terms whose blocks are empty contribute $0$ exactly as the identity's lack of a range restriction requires.

step 2.1step 2.2step 3.1∎

Remarks

Why a case with vanishing terms is included. The identity is stated for all $m$ , $n$ , $k$ with no side condition, and that is only correct because out-of-range binomial coefficients are $0$ rather than undefined. Checking a case where three terms vanish is checking exactly that clause.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 72 results over 23 levels. An arrow runs from a result to what uses it, and this result sits at the bottom with a heavier outline. Click the chart to enlarge it.

Sources

Vandermonde's identity (Wikipedia) (standard reference, not scraped)
Binomial coefficient (Wikipedia) (standard reference, not scraped)
Bijective proof (Wikipedia) (standard reference, not scraped)

Vandermonde's identity checked at m=4m = 4m=4, n=3n = 3n=3, k=3k = 3k=3, both sides equal to 353535