The $1/3$ -- $2/3$ conjecture

Open

FCP.Order.one_third_two_thirds_conjecture

by Lucas · Sep 15, 2026 · Mathlib 0df444a (Lean v4.33.1)

combinatoricsorder

The $1/3$ -- $2/3$ conjecture (Kislitsyn; Fredman; Linial). In every finite partially ordered set that is not totally ordered there are two elements $x, y$ such that the proportion of linear extensions in which $x$ precedes $y$ lies in $[1/3, 2/3]$ . Equivalently, sorting a finite poset by comparisons always admits a nearly balanced query. The best unconditional bound replaces $1/3$ by $(5-\sqrt5)/10 \approx 0.276$ (Brightwell--Felsner--Trotter); the conjecture is known for width-two posets, for semiorders and for several other classes.

Preamble

import Mathlib
import Definitions.Def_FCP_LinearExtensions

Formal statement

namespace FCP.Order

theorem one_third_two_thirds_conjecture (P : Type) [Fintype P] [PartialOrder P]
    (h_not_total : ¬ ∀ x y : P, x ≤ y ∨ y ≤ x) :
    ∃ x y : P, (({e ∈ LinearExtensions P | e x < e y}.ncard : ℚ) /
      (LinearExtensions P).ncard) ∈ Set.Icc (1 / 3 : ℚ) (2 / 3) := by sorry

end FCP.Order

Source

Formal Conjectures library (Google DeepMind), Apache-2.0, https://github.com/google-deepmind/formal-conjectures (FormalConjectures/Wikipedia/conjecture_1_3_to_2_3.lean); https://en.wikipedia.org/wiki/1/3%E2%80%932/3_conjecture

Read-back

What the Lean code literally says, in plain math · Aristotle by Harmonic (non-blind: same agent that drafted the statements)

Non-blind read-back. This read-back was not written by an independent blind auditor: it was written by the same agent that drafted the Lean statement, with full knowledge of the intended meaning and of the source material. It is therefore not independent testimony and must not be mistaken for it; a reviewer who wants genuine blind testimony should commission it separately.

Let $P$ be a finite type with a partial order, and assume it is not the case that all pairs of elements are comparable (i.e. there exist $x, y$ with $x \not\le y$ and $y \not\le x$ ).

Write $\mathcal{L}$ for the set of order-preserving bijections $e$ from $P$ onto $\{0, \dots, |P|-1\}$ . The conclusion asserts the existence of elements $x, y \in P$ such that the rational number

\frac{\#\{e \in \mathcal{L} : e(x) < e(y)\}}{\#\mathcal{L}}

lies in the closed interval $[1/3, 2/3]$ , where $\#$ denotes the natural-number cardinality of a set (which is $0$ for infinite sets, not relevant here).

Points to note: $x$ and $y$ are not required to be distinct or incomparable; the interval is closed at both endpoints; the counting is over order-preserving bijections onto an initial segment, which is the standard model of linear extensions; and if $\mathcal{L}$ were empty the quotient would be $0/0 = 0$ , which is not in $[1/3, 2/3]$ , so the statement implicitly requires linear extensions to exist (they always do for a finite poset).

Human review

Endorsed by Shuze Chen · Sep 17, 2026
Endorsed by Lucas · Sep 17, 2026
Confirmed by the mission captain (proposal self-audit).

View graph

The 1/31/31/3--2/32/32/3 conjecture

The $1/3$ -- $2/3$ conjecture