Alphabeta Math
Session-authored (Fable 5 assisted)
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 P4P_4 is a maximal matching but the two end edges form a larger matching

Counterexample

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

Facts & Assumptions

Given: The path P4P_4 and its middle-edge matching M={23}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 1212 and 3434 each meet 2323, so neither can be added to MM; hence MM is maximal.

given
1.2

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

L1
2.1

Independently, {12,34}\{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={x1,x2,x3}X=\{x_1,x_2,x_3\}, right part Y={a,b}Y=\{a,b\}, and all six possible edges between the two parts. This graph has no matching saturating XX.

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=XS=X, the neighbourhood is N(S)={a,b}N(S)=\{a,b\}, so N(S)=2<3=S|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.

L1
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 A1={a,b}A_1=\{a,b\}, A2={b,c}A_2=\{b,c\}, and A3={a,c}A_3=\{a,c\}, the assignment r(1)=ar(1)=a, r(2)=br(2)=b, r(3)=cr(3)=c is an SDR.

Facts & Assumptions

Given: The three finite sets A1,A2,A3A_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}\{a,b,c\}, and the three-set union is {a,b,c}\{a,b,c\}; the Hall union inequalities all hold.

givenconstruct
1.2

By [L1], the family has an SDR.

L1
2.1

The displayed assignment chooses an element of each AiA_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 →

K3K_3 has ν(K3)=1<2=τ(K3)\nu(K_3)=1<2=\tau(K_3), so König's equality needs bipartiteness

Counterexample

In the triangle K3K_3, every matching has at most one edge, while every vertex cover has at least two vertices. Hence ν(K3)=1<2=τ(K3)\nu(K_3)=1<2=\tau(K_3).

Facts & Assumptions

Given: The complete graph K3K_3 on three vertices.

[L1]

Verification

Verification technique: direct.

1.1

Any two edges of K3K_3 share a vertex, so a matching has at most one edge; any one edge gives ν(K3)=1\nu(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 τ(K3)=2\tau(K_3)=2.

1.3

Thus ν(K3)<τ(K3)\nu(K_3)<\tau(K_3), and [L1] shows precisely why this does not contradict König's theorem: K3K_3 is not bipartite.

L1
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,ts,u,v,t, with labelled arcs and capacities s ⁣u:3,s ⁣v:2,u ⁣v:1,u ⁣t:2,v ⁣t:3.s\!\to u:3,\quad s\!\to v:2,\quad u\!\to v:1,\quad u\!\to t:2,\quad v\!\to t:3. The flow with values 3,2,1,2,33,2,1,2,3 in that order has value five and is maximum.

Facts & Assumptions

Given: The displayed finite integral network and flow ff.

[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 uu, incoming flow 33 equals outgoing flow 1+21+2, and at vv, incoming flow 2+12+1 equals outgoing flow 33; every arc value is within its capacity.

given
1.2

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

1.3

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

L1
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 K2,3K_{2,3}, the two vertices in the two-part have three internally disjoint paths and a minimum separator of size three

Example

Let K2,3K_{2,3} have two-part {x1,x2}\{x_1,x_2\} and three-part {y1,y2,y3}\{y_1,y_2,y_3\}. The paths x1yix2x_1y_ix_2 for i=1,2,3i=1,2,3 are internally vertex-disjoint, and {y1,y2,y3}\{y_1,y_2,y_3\} is a minimum x1x_1-x2x_2 separator.

Facts & Assumptions

Given: The displayed complete bipartite graph K2,3K_{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 x1y1x2x_1y_1x_2, x1y2x2x_1y_2x_2, and x1y3x2x_1y_3x_2 have distinct internal vertices.

given
1.2

Deleting all three yiy_i destroys every x1x_1-x2x_2 path, while deleting fewer leaves some yiy_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.

L1
2.1

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

step 1.1step 1.2step 1.3