What was already known
Pratt’s 2023 preprint, published at STOC 2024, relates the Set Cover Conjecture to the asymptotic rank of balanced tripartitioning tensors and gives a group construction with size 8^k/2. This project proves its optimality among group restrictions and a barrier for combinatorial degenerations, including tensor powers.
AI involvement
Eyal Merhavi chose the problem and directed the research. The project explicitly credits Anthropic Claude agents with the theorem statements, informal proofs and Lean proofs, including the general-group rigidity and tensor-power barrier. Human direction is documented; task-only autonomy is not.
Importance
Closes a specified group-construction route to beating the tensor threshold in Pratt’s Set Cover reduction, including joint constructions on tensor powers. The unrestricted tensor-rank problem remains open.
Limitations
These are bounds on the size of the ambient group and on bounds inherited from this construction method. They do not lower-bound the unrestricted rank or border rank of T_k and do not prove the Set Cover Conjecture. Pratt’s reduction and the passage from an embedding to a rank bound are cited external inputs. Novelty searches were not exhaustive, and no independent human mathematical review is reported.
Technical verification
The exact-commit Palomar preflight job completed its Comparator and challenge-provenance audit on 28 October. The independent statement and proved solution cover the group-size inequalities, commuting-factor rigidity and tensor-power quantifiers; the configuration permits only propext, Classical.choice and Quot.sound. This documents machine checking of these statements. It does not check the cited external Set Cover reduction.
Formal checking
The exact-commit Palomar preflight job completed its Comparator and challenge-provenance audit on 28 October. The independent statement and proved solution cover the group-size inequalities, commuting-factor rigidity and tensor-power quantifiers; the configuration permits only propext, Classical.choice and Quot.sound. This documents machine checking of these statements. It does not check the cited external Set Cover reduction.
- Checker
- Palomar standard mechanical verifier: Lean and Comparator
- Scope
- For k≥2 and m≥1, a Strassen combinatorial degeneration of a finite group tensor onto the mth tensor power of the balanced tripartitioning tensor T_k requires |G|≥binom(3k,⌊3k/2⌋)^m>τ_k^m, where τ_k=8^k binom(3k,k)binom(2k,k)/27^k. For single-copy group restrictions, |G|≥2^{3k−1}; the partition products factor through commuting elements even when G is nonabelian.
- Basis
- Reported by the linked checker
- Check date
- 2026-10-28
Checking a formal statement does not establish that it matches the original problem.
Human understanding
Few is the default when evidence for a higher level is insufficient. No named human explanation of the central rigidity and tensor-power arguments is documented. Agent cross-checks and a generated proof narrative do not establish human understanding.
Correction and publication history
Newly reviewed AI-led general-group rigidity and tensor-power barrier with exact-source machine-check evidence.
Read this published revision