Zakończyłem pełną autoformalizację z @HarmonicMath Arystotelesem następującego ogólnego problemu z teorii grup. Ustal trzy dodatnie liczby całkowite n, k, m. Udowodnij, że podgrupa H grupy S_{6+(n+k+m)} generowana przez 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]>; spełnia H = S_{6+(n+k+m)} lub H = A_{6+(n+k+m)}. Mamy H = S_{6+n+k+m} wtedy i tylko wtedy, gdy przynajmniej jedna z liczb n, k, m jest parzysta, w przeciwnym razie H=A_{6+(n+k+m)}. Repozytorium GitHub z kodem Lean i nieformalnym szkicem ChatGPT-5.1-Pro. Autoformalizacja w dwóch mieszanych uruchomieniach (łącznie około 20 godzin). Kod ma około 2600 linii kodu Lean. Teoremu nie można rozwiązać za pomocą klasycznych systemów algebry komputerowej. Zawiera wcześniejszą próbę z wyborami n=m=k=2 wykonaną wcześniej.