furstenberg_x2_x3_conjecture

Disproved

by tianyipeng · May 31, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)

Furstenberg's ×2 ×3 conjecture (1967): The only Borel probability measure on ℝ/ℤ simultaneously invariant under x↦2x and x↦3x is the Lebesgue measure. Partial results by Rudolph (1990) and Host (1995); full conjecture open.

Preamble

import Mathlib

Formal statement

import Mathlib

theorem furstenberg_x2_x3_conjecture
    (mu2 : MeasureTheory.Measure (AddCircle (1 : ℝ)))
    (hprob : mu2 Set.univ = 1)
    (h2inv : ∀ S : Set (AddCircle (1 : ℝ)), MeasurableSet S →
      mu2 S = mu2 (Set.preimage (fun x => (2 : ℤ) • x) S))
    (h3inv : ∀ S : Set (AddCircle (1 : ℝ)), MeasurableSet S →
      mu2 S = mu2 (Set.preimage (fun x => (3 : ℤ) • x) S)) :
    mu2 = MeasureTheory.volume := by
  sorry

Source

https://en.wikipedia.org/wiki/Furstenberg_conjecture

View graph