Ik heb een volledige auto-formalisatie voltooid met @HarmonicMath Aristotle van het volgende algemene groepentheorieprobleem Neem drie positieve gehele getallen n, k, m. Bewijs dat een groep ondergroep H van S_{6+(n+k+m)} gegenereerd door g1:=G!(1,6,4,3,a_1,...a_n); g2:=G!(1,2,4,5,b_1,...,b_k); g3:=G!(5,6,2,3,c_1,...,c_m); H:=sub<G|[g1,g2,g3]>; voldoet aan H = S_{6+(n+k+m)} of H = A_{6+(n+k+m)}. We hebben H = S_{6+n+k+m} als en alleen als ten minste een van n, k, m even is, anders H=A_{6+(n+k+m)}. GitHub-repo met Lean-code en informele schets van ChatGPT-5.1-Pro De auto-formalisatie in twee gemengde runs (samen ongeveer 20 uur). De code heeft ongeveer 2600 regels Lean-code. De stelling kan niet worden opgelost met klassieke computeralgebrasystemen. Het omvat de eerdere poging met de keuzes n=m=k=2 die eerder is gedaan.