Jeg har fullført en full autoformalisering med @HarmonicMath Aristoteles av følgende generelle gruppeteoriproblem Fiks tre positive heltall n, k, m. Bevis at en gruppeundergruppe H av S_{6+(n+k+m)} generert av 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]>; tilfredsstiller H = S_{6+(n+k+m)} eller H = A_{6+(n+k+m)}. Vi har H = S_{6+n+k+m} hvis og bare hvis minst én av n, k, m er partall, ellers H=A_{6+(n+k+m)}. GitHub-repo med Lean-kode og ChatGPT-5.1-Pro uformell skisse Auto-formaliseringen var i to blandede kjøringer (til sammen omtrent 20 timer). Koden har omtrent 2600 linjer med Lean-kode. Teoremet kan ikke løses med klassiske datamaskinalgebrasystemer. Den legger det forrige forsøket sammen med valgene n=m=k=2 som ble gjort før.