Source labels openChecked July 26, 2026

The $\frac 1 3$–$\frac 2 3$ conjecture

Does every finite partially ordered set that is not totally ordered contain two elements $x$ and $y$ such that the probability that $x$ appears before $y$ in a random linear extension is between $\frac 1 3$ and $\frac 2 3$ ?

Mathematics AMS 6

Mathematical statement

The set of all total order extensions is represented as order preserving bijections $P$ of $1, ..., n$ .

Statement source: Wikipedia statement material

Statement terms: CC-BY-SA-4.0

Attributed source material. Reuse must follow the linked attribution and share-alike terms.

Statement artifacts, not proofs

These records expose exact Lean propositions and statement-only wrappers. Defining a proposition does not supply a proof of it. A placeholder-bearing target also contains no proof. Elaboration checks syntax and types; it does not certify that a formalization perfectly captures every nuance of the informal problem.

Pinned Lean formulation 1

conjecture_1_3_to_2_3

Canonical source

Complete statement target, proof intentionally absentLean 4

theorem conjecture_1_3_to_2_3 : answer(sorry) ↔ ∀ (P : Type) [Finite P] [PartialOrder P]    (not_total : ¬ Std.Total (α := P) (· ≤ ·)) (total_ext : Set <| OrderHom P ℕ)    (total_ext_def : ∀ σ, σ ∈ total_ext ↔ Set.range σ = Set.Icc 1 (Nat.card P)),    ∃ x y : P, ({σ ∈ total_ext | σ x < σ y}.ncard / total_ext.ncard : ℚ)      ∈ Set.Icc (1/3) (2/3) := by  sorry

Statement source: Formal Conjectures
Lean version: v4.27.0
Placeholder: Present; no proof artifact
Source evidence: Pinned source index
Fidelity review: Community formulation

References

Pinned Formal Conjectures sourceformalization Wikipediabackground