Green's Open Problem 85

Suppose that $A$ is an open subset of $[0, 1]^2$ with measure $\alpha$ . Are there four points in $A$ determining an axis-parallel rectangle with area $\gt c \alpha^2$ ?

Measure and integration AMS 28 AMS 52

Mathematical statement

Suppose that $A$ is an open subset of $[0, 1]^2$ with measure $\alpha$ . Are there four points in $A$ determining an axis-parallel rectangle with area $\gt c \alpha^2$ ?

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_85

Canonical source

Complete statement target, proof intentionally absentLean 4

theorem green_85 :  answer(sorry) ↔ ∃ c > 0, ∀ A : Set (ℝ × ℝ),    IsOpen A →    A ⊆ Icc 0 1 ×ˢ Icc 0 1 →    A.Nonempty →    let α := (volume A).toReal    ∃ x₁ x₂ y₁ y₂,      {(x₁, y₁), (x₂, y₁), (x₂, y₂), (x₁, y₂)} ⊆ A ∧      c * α ^ 2 ≤ |x₁ - x₂| * |y₁ - y₂| := 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

Pinned Formal Conjectures sourceformalization Green, Ben. "100 open problems." (2024).background