FormalConjectures/GreensOpenProblems/26.lean
Explanation legend Lean4 Domain Explanation Language (L4DEL)
L4DEL explanations are a separate layer. They do not change the Lean source. Intuition is explanatory prose; numbered items are a reading path; sources link the wording back to evidence.
- L4DEL
- Lean4 Domain Explanation Language
Credit: The upstream authors and contributors retain credit for the project and mathematics. lean4-explainer only renders their pinned source and adds the separately disclosed explanation layer.
Project sources: Pinned project documentation, Formal Conjectures paper, arXiv v1
6 declarations, 4 contain sorry, 0 declared as axioms
Green's Open Problem 26
References:
- [Gr24] Green, Ben. "100 open problems." (2024).
- [JLP92] Jaeger, FranΓ§ois, et al. "Group connectivity of graphsβa nonhomogeneous analogue of nowhere-zero flow properties." Journal of Combinatorial Theory, Series B 56.2 (1992): 165-182.
- [ALM91] Alon, Noga, Nathan Linial, and Roy Meshulam. "Additive bases of vector spaces over prime fields." Journal of Combinatorial Theory, Series A 57.2 (1991): 203-210.
- [Yu25] Yu, Yang. "Note on the Additive Basis Conjecture." arXiv preprint arXiv:2510.01300 (2025).
Imports (1)
- def
Green26.StandardCubeThe standard cube in $\mathbb{F}_p^n$ is the set of points with coordinates in $\{0, 1\}$ line 41 sourceSource documentation
The standard cube in $\mathbb{F}_p^n$ is the set of points with coordinates in $\{0, 1\}$.
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses:
Nat,Fact,Nat.Prime,Set, π½Proof uses:
Set.ofPred,Fin,Or,Eq,ZMod,OfNat.ofNat13 instances, coercions and auxiliary constants left out.
def StandardCube {p : β} [Fact p.Prime] (n : β) : Set (π½ p n) := β¦Mentions: π½
- def
Green26.IsCubeA cube is the image of $\lbrace 0, 1\rbrace^n$ under a linear automorphism line 45 sourceSource documentation
A cube is the image of $\lbrace 0, 1\rbrace^n$ under a linear automorphism.
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses:
Nat,Fact,Nat.Prime,Set, π½Proof uses:
Exists,LinearEquiv,ZMod,RingHom.id,Fin,Eq,Set.image, Green26.StandardCube13 instances, coercions and auxiliary constants left out.
def IsCube {p n : β} [Fact p.Prime] (A : Set (π½ p n)) : Prop := β¦Mentions: π½
- theorem
Green26.green_26Let $A_1, \dots, A_{100}$ be "cubes" in $\mathbb{F}^n_3$ sorry line 53 sourceSource documentation
Let $A_1, \dots, A_{100}$ be "cubes" in $\mathbb{F}^n_3$. Is it true that $A_1 + \dots + A_{100} = \mathbb{F}^n_3$?
depends on sorry what this means
Statement uses:
Nat,Fin,OfNat.ofNat,Set, π½β, Green26.IsCube,Eq,Finset.sum,ZMod,Finset.univ,Set.univProof uses:
sorryAx,Lean.Name,Bool.false,Lean.Name.num,Lean.Name.str,Lean.Name.anonymous20 instances, coercions and auxiliary constants left out.
Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
theorem green_26 : β n : β, β A : Fin 100 β Set (π½β n), (β i, IsCube (A i)) β β i, A i = univ := by β¦Mentions: π½β, Green26.IsCube
- theorem
Green26.green_26.variants.yu25[Yu25] has solved the original problem (with 100 replaced by 4) sorry line 61 sourceSource documentation
[Yu25] has solved the original problem (with 100 replaced by 4)
depends on sorry what this means
Statement uses:
Nat,Fin,OfNat.ofNat,Set, π½β, Green26.IsCube,Eq,Finset.sum,ZMod,Finset.univ,Set.univProof uses:
sorryAx,Lean.Name,Bool.false,Lean.Name.num,Lean.Name.str,Lean.Name.anonymous20 instances, coercions and auxiliary constants left out.
Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
theorem green_26.variants.yu25 : β n : β, β A : Fin 4 β Set (π½β n), (β i, IsCube (A i)) β β i, A i = univ := by β¦Mentions: π½β, Green26.IsCube
- theorem
Green26.green_26.variants.alm91[ALM91] showed that if 100 is replaced by $\leq c(p) \log n$ then the result is true for $\mathbb{F}^n_p$ sorry line 74 sourceSource documentation
[ALM91] showed that if 100 is replaced by $\leq c(p) \log n$ then the result is true for $\mathbb{F}^n_p$.
depends on sorry what this means
Statement uses:
Nat,Fact,Nat.Prime,Exists,And,Asymptotics.IsBigO,Real,Filter.atTop,Real.log,Filter.Eventually,Fin,Set, π½, Green26.IsCube,Eq,Finset.sum,ZMod,Finset.univ,Set.univProof uses:
sorryAx,Lean.Name,Bool.false,Lean.Name.num,Lean.Name.str,Lean.Name.anonymous,OfNat.ofNat25 instances, coercions and auxiliary constants left out.
Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
theorem green_26.variants.alm91 : β (p : β) [Fact p.Prime], β (k : β β β), ((fun n β¦ (k n : β)) =O[atTop] fun n β¦ Real.log n) β§ βαΆ n in atTop, β A : Fin (k n) β Set (π½ p n), (β i, IsCube (A i)) β β i, A i = univ := by β¦Mentions: π½, Green26.IsCube
- theorem
Green26.green_26.variants.openThe analogous problem in $\mathbb{F}^n_p$ remains open sorry line 85 sourceSource documentation
The analogous problem in $\mathbb{F}^n_p$ remains open. [Gr24]
depends on sorry what this means
Statement uses:
Iff,True,Nat,Fact,Nat.Prime,Exists,Fin,Set, π½, Green26.IsCube,Eq,Finset.sum,ZMod,Finset.univ,Set.univProof uses:
sorryAx,Lean.Name,Bool.false,Lean.Name.num,Lean.Name.str,Lean.Name.anonymous,OfNat.ofNat17 instances, coercions and auxiliary constants left out.
Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
theorem green_26.variants.open : answer(sorry) β β (p : β) [Fact p.Prime], (β C, β n, β A : Fin C β Set (π½ p n), (β i, IsCube (A i)) β β i, A i = univ) := by β¦Mentions: π½, Green26.IsCube