Ho completato una formalizzazione automatica completa con @HarmonicMath Aristotele del seguente problema generale di teoria dei gruppi Fissa tre numeri interi positivi n, k, m. Dimostra che un sottogruppo H di S_{6+(n+k+m)} generato da 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]>; soddisfa H = S_{6+(n+k+m)} o H = A_{6+(n+k+m)}. Abbiamo H = S_{6+n+k+m} se e solo se almeno uno tra n, k, m è pari, altrimenti H=A_{6+(n+k+m)}. Repo GitHub con codice Lean e schizzo informale di ChatGPT-5.1-Pro La formalizzazione automatica in due esecuzioni miste (complessivamente circa 20 ore). Il codice ha circa 2600 righe di codice Lean. Il teorema non può essere risolto con sistemi classici di algebra computazionale. Sussume il tentativo precedente con le scelte n=m=k=2 effettuato in precedenza.