ExampleConstruction: Literature-sourcedVerification: AI-adaptedprecheck passjudge pass (gpt-5.6-terra)audited 2026-09-04

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.

Bertrand's chord paradox is a model-specification problem

Example

Consider a circle of radius $1$ and the event that a random chord is longer than the side of the inscribed equilateral triangle. Three natural models give three different probabilities.

If the chord is determined by a random central angle $Θ \sim U n i f [0, π]$ , then the event is ${Θ > 2 π / 3}$ and has probability $1 / 3$ .
If the chord is determined by choosing its midpoint uniformly on a fixed radius, then the event is that the midpoint lies within distance $1 / 2$ of the center, and has probability $1 / 2$ .
If the chord is determined by choosing its midpoint uniformly in the whole disk, then the same geometric condition gives probability $1 / 4$ .

Facts & Assumptions

Given: The three sample-space models stated in the Example.

[L1]

A probability question is determined only after the sample space and its probability measure have been fixed (Probability measures and probability spaces).

Verification

technique · direct

1.1

A chord subtending central angle $Θ$ has length $2 \sin (Θ / 2)$ . It is longer than $\sqrt{3}$ exactly when $\sin (Θ / 2) > \sqrt{3} / 2$ , that is, when $Θ > 2 π / 3$ . Under the uniform-angle model this has probability $(π - 2 π / 3) / π = 1 / 3.$

L1givenalgebra

2.1

A chord is longer than $\sqrt{3}$ exactly when its midpoint is within distance $1 / 2$ of the center. Along a fixed radius, the favorable segment has length $1 / 2$ inside the unit segment, so the midpoint-on-a-radius model gives probability $1 / 2$ . Over the whole disk, the favorable region is the disk of radius $1 / 2$ , so the midpoint-in-the-disk model gives area ratio $(π (1 / 2)^{2}) / π = 1 / 4.$

step 1.1L1algebra

3.1

The three different answers $1 / 3$ , $1 / 2$ , and $1 / 4$ come from three different probability models for the same geometric question, exactly as [L1] predicts.

step 1.1step 2.1L1∎

Depends on

Probability measures and probability spaces

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

3 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

Jean-Francois Le Gall, Integration, Probabilities and Stochastic Processes, Section 8.1.4 (standard reference, not scraped)