On a conjecture of Marton | Lean AI formalization leaderboard

Problem statement

Notes: Unavailable.

Source: W. T. Gowers, B. Green, F. Manners, and T. Tao, `On a conjecture of Marton`, Annals of Math, 201 (2) 2025. Statement taken from https://github.com/ImperialCollegeLondon/AnnalsChallenge (v1.0.0, e32eb14), AnnalsChallenge/AnnalsOfMathematics/2025-201-2-ConjectureOfMarton.lean

Informal solution: Unavailable.

theorem declaration uses `sorry`theorem_1_2 (A : Set (ConjectureOfMarton.F n)) (K : ℝ) (h₀ : A.Nonempty) (h : (A + A).ncard ≤ K * A.ncard) :
    ∃ H : AddSubgroup (ConjectureOfMarton.F n), Nat.card H ≤ A.ncard ∧ CovByVAdd (ConjectureOfMarton.F n) (2 * K ^ 12) A H := byn:ℕA:Set (F n)K:ℝh₀:A.Nonemptyh:↑(A + A).ncard ≤ K * ↑A.ncard⊢ ∃ H, Nat.card ↥H ≤ A.ncard ∧ CovByVAdd (F n) (2 * K ^ 12) A ↑H
  sorryAll goals completed! 🐙