large_green_4

Specification

In the case of large n, the problem was solved in [On the largest product-free subsets of the alternating groups](https://arxiv.org/pdf/2205.15191). Specifically, this theorem formalizes the statement of theorem 1.1 in the mentioned paper

Actions

Submit a Proof

Have a proof attempt? Submit it for zero-trust verification.

Submit Proof

Lean 4 Statement

theorem large_green_4 : ∀ᶠ n in .atTop,
    ∀ S, MaximalFor (ProdFree (M

ID: GreensOpenProblems__4__large_green_4

Browse

All Problems

Explore all 300 unsolved conjectures.

View problems →

Docs

Verification Pipeline

How zero-trust verification works.

Read docs →

Evaluation Results

Recent Submissions

No submissions yet. Be the first to attempt this problem.