AI Proof WatchKeep up with AI contributions

Claude-led proof gives a logarithmic symmetric-group word threshold

For nonzero integers r,s with at least one odd, the word xʳyˢ is universal in Sₙ once n is sufficiently large and at least C log m(r,s), where m is the product of the distinct primes dividing rs. A separate construction shows the logarithmic order cannot generally be reduced.

Sources for this record

What was already known

Kourovka Notebook Problem 10.32 asks for the symmetric-group case. Droste’s earlier bound was linear in m(r,s); the alternating-group result and eight classical inputs predate this work.

AI involvement AI-led

Kondareddy set the goal and reviewed outcomes. Claude Fable 5 and Opus 5 agents produced the argument and Lean proof.

The agents supplied the mathematical proof and formalization under Kondareddy's goals and acceptance decisions; the source does not establish full autonomy from human direction.

Importance Notable

Gives a logarithmic-order answer to the named symmetric-group word problem, subject to the cited input theorems.

Limitations

The checked positive theorem is an implication from eight stated published results; the unconditional wrapper takes them as axioms. The formal check does not certify the paper’s numerical C=4.65, and the match between all eight hypotheses and their literature sources has not been independently established.

Technical verification Formal (Lean 4 kernel with Mathlib, axiom audit and Comparator)

The complete conditional implication and the lower-bound construction are reported as sorry-free Lean theorems with standard axioms and Comparator comparison. This Formal rating applies to the stated conditional result and separately checked obstruction. The eight literature premises were not proved in Lean and the unconditional wrapper adds them as axioms.

Independent checking

Sorry-free kernel proofs, standard-axiom audit and statement comparison; the eight inputs remain explicit hypotheses

Checker
Lean kernel and Comparator in Kondareddy's pinned repository
Scope
UniversalWords.kourovka_10_32_conditional from eight named input statements and UniversalWords.not_universal lower-bound construction
Basis
Reported by the linked checker
Evidence source

Human understanding Few

Default for missing human explanation: Kondareddy reviewed outcomes, but the prose proof and referee rounds were agent-produced and no human mathematical account of the mechanism is documented.

Correction and publication history

2026-10-18 · publication

Gives a logarithmic-order answer to the named symmetric-group word problem, subject to the cited input theorems.

Read this published revision