Green's open problem 54

Let

K \subset \mathbb{R}^n

be a balanced compact set (that is,

\lambda K \subseteq K

whenever

|\lambda| \leq 1

) and suppose that the normalised Gaussian measure

\gamma_n(K) \geq 0.99

. Does

10K

contain a compact convex set

C

with

\gamma_n(C) \geq 0.01

Withdrawn 5 Aug 2026

SOURCE_MISMATCH (Green #54 is per-n on ℝ^n; formalization is a single statement on ℕ → ℝ with Measure.infinitePi gaussian — nonequivalent setting)

Formal statement

Proof target

import FormalConjectures.GreensOpenProblems.«54»
import TaskSupport

namespace Bounty

theorem target : fcTypeOfName% "Green54.green_54" := by
  sorry

end Bounty

Open this target’s Challenge.lean

Original conjecture (Lean type)

True ↔
  ∀ (K : Set (ℕ → ℝ)),
    IsCompact K →
      Balanced ℝ K →
        0.99 ≤ Green54.gaussianMeasureInf K →
          ∃ C, IsCompact C ∧ Convex ℝ C ∧ C ⊆ 10 • K ∧ 1e-2 ≤ Green54.gaussianMeasureInf C

Original conjecture source: FormalConjectures/GreensOpenProblems/54.lean

Task id: fc-379fc029-green54-green-54-6ec57c163e-formalized-v1
Task commitment: sha256:5f2f6f4d6960b6b8ac53df6624428065451a5732d2e0d834f40d10038d984c9a

References

Ben Green's Open Problem 54

Original formulation: M. Talagrand, Are All Sets of Positive Measure Essentially Convex?, in Operator Theory:

Something wrong with this formalization?

A statement that does not faithfully capture the original conjecture is the one real risk here, so we would rather hear about it early - before someone spends weeks on it.

Our channel is in the Bittensor Discord server. Join the server first, then open the channel to send your report.

Bittensor Discord