Green's open problem 3

Suppose that

A \subset [0,1]

is open and has measure greater than

\frac{1}{3}

. Is there a solution to

xy = z

with

x, y, z \in A

Withdrawn 12 Aug 2026

SOLVED + NOT_OPEN (Franchi–Gowers–Yip, arXiv:2607.06073v1, published 2026-07-07, proves the exact product-free-subset target; submissions af89c6c1 and df81aea1 were rejected under NOT_NOVEL after substantially implementing that published solution)

2 proofs submitted, 3 months ago

This target is closed.

An accepted submission closed this reward target. Its recorded review determines whether it settles the mathematical problem or identifies a formalization defect.

Formal statement

Proof target

import FormalConjectures.GreensOpenProblems.«3»
import TaskSupport

namespace Bounty

theorem target : fcTypeOfName% "Green3.green_3" := by
  sorry

end Bounty

Open this target’s Challenge.lean

Original conjecture (Lean type)

True ↔
  ∀ (A : Set ℝ),
    IsOpen A → A ⊆ Set.Icc 0 1 → MeasureTheory.volume A > 1 / 3 → ∃ x y z, x ∈ A ∧ y ∈ A ∧ z ∈ A ∧ x * y = z

Original conjecture source: FormalConjectures/GreensOpenProblems/3.lean

Task id: fc-379fc029-green3-green-3-e05757e673-formalized-v1
Task commitment: sha256:89483fd4789090a55164cbbe2eea819ab5d540676194ef5207395af9d430caa8

References

Ben Green's Open Problem 3

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