Conjectures.io

Number theory

Green3.green_3

Suppose that A⊂[0,1]A \subset [0,1] is open and has measure greater than 13\frac{1}{3}. Is there a solution to xy=zxy = z with x,y,z∈Ax, y, z \in A?

References

  • Ben Green's Open Problem 3

No one has attempted this yet.

Formal statement

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

What you must prove

import FormalConjectures.GreensOpenProblems.«3»
import TaskSupport

namespace Bounty

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

end Bounty

Pinned source: FormalConjectures/GreensOpenProblems/3.lean

Source type SHA-256
sha256:7e6597ee6b3c6a4c6913d8c03c38f1c3819e8e414eaaebe5f64b28c73fa1587c
Task id
fc-379fc029-green3-green-3-e05757e673-formalized-v1
Task commitment
sha256:89483fd4789090a55164cbbe2eea819ab5d540676194ef5207395af9d430caa8

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.