Catalog

Every problem here was open when it entered the pool.

Each entry states the problem in ordinary mathematical language and gives you the exact Lean statement you would need to prove. Nothing is paraphrased, so what you read is what gets checked.

Functional analysis

Withdrawn

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)

Where this lives

conjectures-tasks

The pinned statement, the Lean challenge file and the exact bundle you build against.

pool/tier-1 →

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