Alphabeta Math
CounterexampleConstruction: AI-adaptedVerification: AI-generatedSession-authored (Fable 5 assisted)precheck passaudited 2026-07-31
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.

When k<n<2kk<n<2k, the entire kkth level is intersecting and exceeds the Erdős-Ko-Rado star bound

Statement refuted

The false statement False: the Erdős-Ko-Rado bound holds without the hypothesis n≥2kn\ge 2k claims the Erdős-Ko-Rado star bound without assuming n≥2kn\ge2k.

Facts & Assumptions

Given: Natural numbers satisfying exactly k<n<2kk<n<2k, an nn-element set AA, and the full level F=[A]k\mathcal F=[A]^k.

[F1]

An intersecting family has nonempty intersection between every pair of members, and (nk)=∣[A]k∣\binom nk=|[A]^k| (Intersecting uniform families of finite sets, The set [A]k[A]^{k} of kk-element subsets and the binomial coefficient (nk):=∣[n]k∣\binom{n}{k} := \lvert [n]^{k}\rvert).

[L1]

The binomial closed formula gives (nk)=nk(n−1k−1)\binom nk=\frac n k\binom{n-1}{k-1} for 1≤k≤n1\le k\le n ((nk) k! (n−k)!=n!\binom{n}{k}\,k!\,(n-k)! = n! for k≤nk \le n; hence (nk) k!=nk‾\binom{n}{k}\,k! = n^{\underline{k}}, the quotient n!/(k!(n−k)!)n!/(k!(n-k)!) is a natural number, and (nk)=(nn−k)\binom{n}{k} = \binom{n}{n-k}).

Counterexample

technique · direct
1.1

If S,T∈[A]kS,T\in[A]^k were disjoint, then ∣S∪T∣=2k>n=∣A∣|S\cup T|=2k>n=|A|, impossible. Hence the entire level F\mathcal F is intersecting.

givenF1
1.2

By [L1], ∣F∣=(nk)=(n/k)(n−1k−1)|\mathcal F|=\binom nk=(n/k)\binom{n-1}{k-1}. Since k<nk<n, the factor n/kn/k is greater than 11, so ∣F∣>(n−1k−1)|\mathcal F|>\binom{n-1}{k-1}.

givenF1L1algebra
2.1

Thus for every k<n<2kk<n<2k, the full kkth level is an intersecting family larger than a star, refuting the bound outside its stated range.

step 1.1step 1.2∎

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: 67 results over 24 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