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.

✓ 1 result · 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 1 not AI-judged were verified by owner audit (typically over a confirmed judge false positive), not failures.

The Fundamental Group — Examples

1 · Prerequisites

2 · Summary

3 · Logical flowchart

4 · Definitions, theorems and proofs

None yet.

5 · Examples, counterexamples and false statements

ExampleConstruction: Literature-sourcedVerification: AI-adaptedprecheck passaudited 2026-08-03Open item page →

The fundamental group of the unit interval is trivial at every basepoint

Example

For every x0∈I=[0,1]x_0\in I=[0,1], the fundamental group π1(I,x0)\pi_1(I,x_0) has one element. A loop α\alpha contracts relative to its endpoints by

H(s,t)=(1−t)α(s)+tx0.H(s,t)=(1-t)\alpha(s)+t x_0.

Facts & Assumptions

Given: A basepoint x0∈Ix_0\in I and a based loop α:I→I\alpha:I\to I.

[L1]

The unit interval is convex: if x,y,t∈[0,1]x,y,t\in[0,1], then 0≤(1−t)x+ty≤10\le(1-t)x+ty\le1, so the convex combination remains in [0,1][0,1] (Intervals of R\mathbb{R}: the nine order-convex forms, nondegeneracy, and length, A convex subset of Rm\mathbb{R}^m contains every line segment between two of its points, algebra).

[L2]

Every nonempty convex Euclidean subset is simply connected, with the displayed straight-line endpoint homotopy (Every nonempty convex subset of Rn\mathbb R^n is simply connected).

[L3]

Elements of π1(I,x0)\pi_1(I,x_0) are endpoint-homotopy classes of based loops (Based loops and the fundamental group).

Verification

technique · direct
1.1

By [L1], the interval satisfies the hypotheses of [L2], so the displayed formula is an endpoint-fixed homotopy from α\alpha to the constant loop at x0x_0.

L1L2
2.1

Thus every class in π1(I,x0)\pi_1(I,x_0) equals the constant-loop class, and the group has exactly one element.

step 1.1L3∎

Sources

Standard references

Recommended treatments; not extraction sources.