OP-00018 Open

The 1/3–2/3 conjecture for finite posets

Let $P$ be a finite partially ordered set that is not a chain. Are there two elements $x, y \in P$ such that, in a linear extension of $P$ chosen uniformly at random, $x$ comes before $y$ with probability between $1/3$ and $2/3$?

Source: S. S. Kislitsyn, Mat. Zametki 4 (1968); independently M. L. Fredman, Theoret. Comput. Sci. 1 (1976), and N. Linial, SIAM J. Comput. 13 (1984).

Classification

Primary: CO — Combinatorics
Keywords: linear extensions, partially ordered sets, sorting

References

@article{kislitsyn1968,
  author = {Kislitsyn, S. S.},
  title = {A finite partially ordered set and its corresponding set of permutations},
  journal = {Matematicheskie Zametki},
  volume = {4},
  pages = {511--518},
  year = {1968}
}

@article{fredman1976,
  author = {Fredman, Michael L.},
  title = {How good is the information theory bound in sorting?},
  journal = {Theoretical Computer Science},
  volume = {1},
  pages = {355--361},
  year = {1976}
}

@article{linial1984,
  author = {Linial, Nathan},
  title = {The information-theoretic bound is good for merging},
  journal = {SIAM Journal on Computing},
  volume = {13},
  pages = {795--801},
  year = {1984}
}

@article{bft1995,
  author = {Brightwell, Graham R. and Felsner, Stefan and Trotter, William T.},
  title = {Balancing pairs and the cross product conjecture},
  journal = {Order},
  volume = {12},
  pages = {327--349},
  year = {1995}
}

@misc{wikipedia,
  title = {1/3–2/3 conjecture},
  howpublished = {Wikipedia},
  url = {https://en.wikipedia.org/wiki/1/3%E2%80%932/3_conjecture}
}

@misc{formalconjectures,
  author = {{The Formal Conjectures Authors}},
  title = {Formal Conjectures},
  url = {https://github.com/google-deepmind/formal-conjectures/blob/0771383387505c96d1b2f6a3d35088ad00892c5c/FormalConjectures/Wikipedia/conjecture_1_3_to_2_3.lean#L30},
  note = {Lean statement under Apache-2.0; problem text under CC BY 4.0, or CC BY-SA 4.0 where it is based on Wikipedia}
}

Canonical Lean statement

A submission resolves this problem by proving the constant Problem_OP_00018.

/-- OP-00018: The 1/3–2/3 conjecture for finite posets -/
def Problem_OP_00018 : Prop :=
  ∀ (P : Type) [Finite P] [inst : PartialOrder P],
      (¬Std.Total fun (x1 x2 : P) ↦ x1 ≤ x2) →
        ∀ (total_ext : Set (P →o ℕ)),
          (∀ (σ : P →o ℕ), σ ∈ total_ext ↔ Set.range (⇑σ : P → ℕ) = Set.Icc (1 : ℕ) (Nat.card P)) →
            ∃ (x : P) (y : P),
              (↑(Set.ncard {σ : P →o ℕ | σ ∈ total_ext ∧ (σ : P → ℕ) x < (σ : P → ℕ) y}) : ℚ) /
                  (↑(Set.ncard total_ext) : ℚ) ∈
                Set.Icc (1 / 3 : ℚ) (2 / 3 : ℚ)

Formalised by The Formal Conjectures Authors (Apache-2.0); reviewed by clemens-admin.

Available to match against in: Lean v4.33.1 with Mathlib v4.33.1.

Resolving this problem in Lean

Add the problems package as a dependency, import this problem's module, and prove the constant. Any published revision works.

In lakefile.toml:

[[require]]
name = "RegistryProblems"
git = "https://github.com/cthalhammer/registry-problems"
rev = "<published revision>"

In your proof:

import RegistryProblems.OP_00018

theorem resolution : RegistryProblems.Problem_OP_00018 := by
  sorry

In preprint.toml, mapping the claim to the declaration that establishes it:

[[statements]]
label = "Theorem 1"
lean = "resolution"
latex = "..."
problem = "OP-00018"
claim = "full"

To disprove it instead, prove the negation and claim "disproof", or "counterexample" if the proof exhibits one:

theorem disproof : ¬ RegistryProblems.Problem_OP_00018 := by
  sorry

You can also write the statement out in full; the verifier checks it matches up to definitional equality. Partial results and reductions are not matched against this statement.

Citing this problem

This identifier is permanent. It will not change if the problem is solved, reclassified or withdrawn.

OP-00018, "The 1/3–2/3 conjecture for finite posets", clopen.solutions.