All open problems
Source labels openChecked July 26, 2026
Green's Open ProblemsCombinatorics
Green's Open Problem 52
Could even contain a coset of codimension ?
Mathematical statement
Could even contain a coset of codimension ?
Statement source: Green's Open Problems statement material
Statement terms: Source-specific
Source-specific terms. Therefore does not assert reuse rights beyond attributed display.
Statement artifacts, not proofs
These records expose exact Lean propositions and statement-only wrappers. Defining a proposition does not supply a proof of it. A placeholder-bearing target also contains no proof. Elaboration checks syntax and types; it does not certify that a formalization perfectly captures every nuance of the informal problem.
Pinned Lean formulation 1
green_52_log
Complete statement target, proof intentionally absentLean 4
theorem green_52_log : answer(sorry) ↔ ∃ (C D : ℝ), ∀ (n K : ℕ) (A : Set (𝔽₂ n)) (S : Finset (𝔽₂ n)), 0 < K → S.card = K → A + (S : Set (𝔽₂ n)) = Set.univ → ∃ (V : AffineSubspace (ZMod 2) (𝔽₂ n)), (V : Set (𝔽₂ n)) ⊆ A + A ∧ (n : ℝ) ≤ (Module.finrank (ZMod 2) V.direction : ℝ) + C * log (K : ℝ) + D := by sorry- Statement source
- Formal Conjectures
- Lean version
- v4.27.0
- Placeholder
- Present; no proof artifact
- Source evidence
- Pinned source index
- Fidelity review
- Community formulation
References