Conjectures.io

submission

Green's open problem 3

Lean accepted this proof on 6 Aug 2026. What happens to it next is decided by people, and that decision is recorded below.

Review decision

Already solved before this submissionNOT_NOVEL

Rejected under NOT_NOVEL pursuant to manual-review policy v2. The Gowers–Franchi–Yip paper “Product-free subsets of (0,1)” (arXiv:2607.06073v1) was public on 2026-07-07 and proves the exact Green 3 target: every open product-free subset of (0,1) has measure at most 1/3. This submission was accepted on 2026-08-06. The submitted Lean proof substantially implements that source’s distinctive solution for the same target. In both, the product-free problem is transported by x ↦ −log x to a sum-free-set problem; discrepancy and balanced-interval machinery is developed; the central finite-union-of-closed-intervals inequality f(u−1)+f(u)+f(u+1) ≤ u is proved; and the result is returned to the open-set target through the exponentially weighted integral and cosh bound. The submission supplies a formal inward-approximation bridge from open sets to finite unions of closed intervals, but that bridge completes the same published argument rather than constituting a different solution to the direct problem. This is a bounty-novelty classification, not a finding of plagiarism or misattribution. The public statement that Aristotle had formalized the paper was not relied upon because no inspectable target-specific artifact was established. The earlier Green 3 submission was ineligible, so duplicate-submission status is not the basis for this decision. The submitter may request reconsideration and provide contrary chronology or source-correspondence evidence. Source: https://arxiv.org/abs/2607.06073v1 Review criteria: https://github.com/conjectures-io/conjectures-validator/blob/main/docs/MANUAL_REVIEW_CRITERIA.md

Rejected · decided 7 Aug 2026

Formal statement

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

Verification report

Every box below had to hold before the proof counted. They are grouped in the order the verifier reaches them.

The task it was checked against

  • Manifest valid — Passed

    The task bundle held together: the exact file set, a strict manifest, and every trusted hash matching the bytes on disk.

  • Task commitment matches — Passed

    The bundle digest the submission committed to is the digest of the bundle that was actually verified.

  • Production task — Passed

    The task came from the production pool rather than a test fixture.

  • Trusted file hashes match — Passed

    The pinned dependencies agree across the manifest, the lockfile and the checkout, down to the same Formal Conjectures commit.

The submission and the sandbox

  • Submission policy respected — Passed

    The submitted source passed the static scan: no imports, no axiom declarations, no sorry, no native_decide, no unsafe options.

  • Production sandbox — Passed

    The run happened under real isolation, Landrun with seccomp, and the sandbox passed its own live self-test before the proof was touched.

The trusted build

  • Challenge built — Passed

    The trusted Challenge.lean, which contains no miner code, compiled on its own.

  • Source type hash matches — Passed

    The source theorem in the compiled environment still hashes to the type recorded in the task, so the statement has not drifted upstream.

The kernel's verdict

  • Solution built — Passed

    The submitted Solution.lean compiled.

  • Statement unchanged — Passed

    The theorem the proof establishes has exactly the same canonical type as the task's target - it was not weakened or restated.

  • Only permitted axioms — Passed

    The transitive axiom closure of the proof stays inside the axioms this task permits.

  • Lean kernel accepted — Passed

    The Lean kernel replayed the proof and accepted it.

  • Nanoda accepted — Not run

    A second kernel, written independently of Lean's, also accepted the proof.

One kernel, not two

This task does not require a second, independent kernel, so Nanoda was not run. The verdict rests on a single kernel implementation.

Theorems established

  • Bounty.target

Stage COMPLETED · Axioms permitted: propext, Quot.sound, Classical.choice