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.

✓ 6 results · all verified · 0 also independently AI-judged

Every result on this page is machine-checked by a proof checker and read in full and owner-audited; the judge is an additional, independent cross-model AI review of the proofs. The 6 not AI-judged were verified by owner audit (typically over a confirmed judge false positive), not failures.

Matchings, Covers, Menger and Network Flows — Examples

1 · Prerequisites

2 · Summary

3 · Logical flowchart

4 · Definitions, theorems and proofs

None yet.

5 · Examples, counterexamples and false statements

CounterexampleConstruction: AI-generatedVerification: AI-generatedprecheck passaudited 2026-08-02Open item page →

The middle edge of $P_{4}$ is a maximal matching but the two end edges form a larger matching

Counterexample

Let $P_{4}$ have consecutive vertices $1, 2, 3, 4$ and let $M = {23}$ . Then $M$ is maximal but not maximum: ${12, 34}$ is a matching of size two.

Facts & Assumptions

Given: The path $P_{4}$ and its middle-edge matching $M = {23}$ .

[L1]

A matching is maximum exactly when it has no augmenting path (Berge's theorem: a matching is maximum if and only if it has no augmenting path).

Verification

Verification technique: direct.

1.1

The two remaining edges $12$ and $34$ each meet $23$ , so neither can be added to $M$ ; hence $M$ is maximal.

given

1.2

The path $1, 2, 3, 4$ is $M$ -augmenting, and [L1] therefore also shows that $M$ is not maximum.

2.1

Independently, ${12, 34}$ is a disjoint two-edge matching, so the maximal and maximum notions differ in this finite path.

step 1.1step 1.2∎

ExampleConstruction: AI-generatedVerification: AI-generatedprecheck passaudited 2026-08-02Open item page →

Three left vertices with only two collective neighbours fail Hall's condition and cannot all be matched

Example

Take left part $X = {x_{1}, x_{2}, x_{3}}$ , right part $Y = {a, b}$ , and all six possible edges between the two parts. This graph has no matching saturating $X$ .

Facts & Assumptions

Given: The displayed finite bipartite graph.

[L1]

A finite bipartite graph has a matching saturating its left part exactly when Hall's condition holds (Hall's marriage theorem for a finite bipartite graph).

Verification

Verification technique: direct.

1.1

For $S = X$ , the neighbourhood is $N (S) = {a, b}$ , so $∣ N (S) ∣ = 2 < 3 = ∣ S ∣$ .

given

1.2

Thus Hall's condition fails, and [L1] proves that no matching can saturate all three left vertices.

2.1

The two available right vertices also show directly that any matching has at most two edges.

step 1.1step 1.2∎

ExampleConstruction: AI-generatedVerification: AI-generatedprecheck passaudited 2026-08-02Open item page →

A three-set family with an explicit system of distinct representatives

Example

For $A_{1} = {a, b}$ , $A_{2} = {b, c}$ , and $A_{3} = {a, c}$ , the assignment $r (1) = a$ , $r (2) = b$ , $r (3) = c$ is an SDR.

Facts & Assumptions

Given: The three finite sets $A_{1}, A_{2}, A_{3}$ .

[L1]

A family with finite index set and finite union has an SDR exactly when every indexed subfamily has union at least as large as its index set (A finite family has an SDR if and only if every subfamily has a union at least as large as its index set).

Verification

Verification technique: constructive.

1.1

Each singleton union has size two, each two-set union is ${a, b, c}$ , and the three-set union is ${a, b, c}$ ; the Hall union inequalities all hold.

givenconstruct

1.2

By [L1], the family has an SDR.

2.1

The displayed assignment chooses an element of each $A_{i}$ and has three distinct values, so it is the promised SDR.

step 1.1step 1.2discharge-construct∎

CounterexampleConstruction: AI-generatedVerification: AI-generatedprecheck passaudited 2026-08-02Open item page →

$K_{3}$ has $ν (K_{3}) = 1 < 2 = τ (K_{3})$ , so König's equality needs bipartiteness

Counterexample

In the triangle $K_{3}$ , every matching has at most one edge, while every vertex cover has at least two vertices. Hence $ν (K_{3}) = 1 < 2 = τ (K_{3})$ .

Facts & Assumptions

Given: The complete graph $K_{3}$ on three vertices.

[L1]

König's equality applies to finite bipartite graphs (König's theorem: $ν (G) = τ (G)$ for every finite bipartite graph).

Verification

Verification technique: direct.

1.1

Any two edges of $K_{3}$ share a vertex, so a matching has at most one edge; any one edge gives $ν (K_{3}) = 1$ .

given

1.2

Deleting one vertex leaves an edge, so one vertex is not a cover; two vertices cover all edges, giving $τ (K_{3}) = 2$ .

1.3

Thus $ν (K_{3}) < τ (K_{3})$ , and [L1] shows precisely why this does not contradict König's theorem: $K_{3}$ is not bipartite.

2.1

This triangle is a finite witness that bipartiteness is a necessary hypothesis for the equality.

step 1.1step 1.2step 1.3∎

ExampleConstruction: AI-generatedVerification: AI-generatedprecheck passaudited 2026-08-02Open item page →

A four-vertex integral network with an exhibited maximum flow and minimum cut of value five

Example

Let the vertices be $s, u, v, t$ , with labelled arcs and capacities $s ⁣ \to u : 3, s ⁣ \to v : 2, u ⁣ \to v : 1, u ⁣ \to t : 2, v ⁣ \to t : 3.$ The flow with values $3, 2, 1, 2, 3$ in that order has value five and is maximum.

Facts & Assumptions

Given: The displayed finite integral network and flow $f$ .

[L1]

Finite integral max-flow min-cut equates a maximum flow value and a minimum cut capacity (Ford-Fulkerson terminates for finite integer capacities and proves max-flow min-cut with an integral maximum flow).

Verification

Verification technique: direct.

1.1

At $u$ , incoming flow $3$ equals outgoing flow $1 + 2$ , and at $v$ , incoming flow $2 + 1$ equals outgoing flow $3$ ; every arc value is within its capacity.

given

1.2

The flow value is $3 + 2 = 5$ , while the cut $S = {s}$ has capacity $3 + 2 = 5$ .

1.3

By [L1], the exhibited feasible flow and cut of common value five are respectively maximum and minimum.

2.1

This network therefore has max-flow value and min-cut capacity both equal to five.

step 1.1step 1.2step 1.3∎

ExampleConstruction: AI-generatedVerification: AI-generatedprecheck passaudited 2026-08-02Open item page →

In $K_{2, 3}$ , the two vertices in the two-part have three internally disjoint paths and a minimum separator of size three

Example

Let $K_{2, 3}$ have two-part ${x_{1}, x_{2}}$ and three-part ${y_{1}, y_{2}, y_{3}}$ . The paths $x_{1} y_{i} x_{2}$ for $i = 1, 2, 3$ are internally vertex-disjoint, and ${y_{1}, y_{2}, y_{3}}$ is a minimum $x_{1}$ - $x_{2}$ separator.

Facts & Assumptions

Given: The displayed complete bipartite graph $K_{2, 3}$ .

[L1]

For nonadjacent terminals, finite vertex Menger equates maximum internally disjoint paths and minimum vertex separators (Menger's theorem: the finite directed and undirected arc, edge and nonadjacent-vertex forms).

Verification

Verification technique: direct.

1.1

The three paths $x_{1} y_{1} x_{2}$ , $x_{1} y_{2} x_{2}$ , and $x_{1} y_{3} x_{2}$ have distinct internal vertices.

given

1.2

Deleting all three $y_{i}$ destroys every $x_{1}$ - $x_{2}$ path, while deleting fewer leaves some $y_{i}$ and its two-edge path.

1.3

The terminals are nonadjacent, so [L1] agrees with the direct calculation: both the packing and separator numbers equal three.

2.1

This is a concrete equality case for the local undirected vertex form.

step 1.1step 1.2step 1.3∎

Matchings, Covers, Menger and Network Flows — Examples

1 · Prerequisites

2 · Summary

3 · Logical flowchart

4 · Definitions, theorems and proofs

5 · Examples, counterexamples and false statements

The middle edge of P4P4​ is a maximal matching but the two end edges form a larger matching

Counterexample

Facts & Assumptions

Verification

Three left vertices with only two collective neighbours fail Hall's condition and cannot all be matched

Example

Facts & Assumptions

Verification

A three-set family with an explicit system of distinct representatives

Example

Facts & Assumptions

Verification

K3K3​ has ν(K3)=1<2=τ(K3)ν(K3​)=1<2=τ(K3​), so König's equality needs bipartiteness

Counterexample

Facts & Assumptions

Verification

A four-vertex integral network with an exhibited maximum flow and minimum cut of value five

Example

Facts & Assumptions

Verification

In K2,3K2,3​, the two vertices in the two-part have three internally disjoint paths and a minimum separator of size three

Example

Facts & Assumptions

Verification

The middle edge of $P_{4}$ is a maximal matching but the two end edges form a larger matching

$K_{3}$ has $ν (K_{3}) = 1 < 2 = τ (K_{3})$ , so König's equality needs bipartiteness

In $K_{2, 3}$ , the two vertices in the two-part have three internally disjoint paths and a minimum separator of size three