Group theory
Approved
A family of 3-approximate subgroups refutes the proposed uniform polynomial lower bound for the size of subsets S satisfying S^8 contained in A^4.
Submitted by 5GeGrY…uLUScV
Withdrawn 6 Aug 2026
SOLVED (approved submission 82ab85ee refutes the published target with a 3-approximate group A = ({-1} × H) ∪ ({+1} × H) ∪ {(0,1)} in Multiplicative ℤ × H, whose only element at coordinate 0 is the identity, so every S ⊆ A with S^8 ⊆ A^4 is a singleton; the formalization is faithful and no defect was found)
Read the recorded decisionFormal statement
Proof target
import FormalConjectures.GreensOpenProblems.«29»
import TaskSupport
namespace Bounty
theorem target : fcTypeOfName% "Green29.green_29" := by
sorry
end Bounty
Original conjecture (Lean type)
True ↔
∃ C c,
0 < C ∧
0 < c ∧
∀ {G : Type u_1} [inst : Group G] [inst_1 : DecidableEq G] (K : ℝ) (A : Finset G),
1 ≤ K → IsApproximateSubgroup K ↑A → ∃ S ⊆ A, C * K ^ (-c) * ↑A.card ≤ ↑S.card ∧ S ^ 8 ⊆ A ^ 4Original conjecture source: FormalConjectures/GreensOpenProblems/29.lean
References
Something wrong with this formalization?
A statement that does not faithfully capture the original conjecture is the one real risk here, so we would rather hear about it early - before someone spends weeks on it.
Our channel is in the Bittensor Discord server. Join the server first, then open the channel to send your report.