Ich habe eine vollständige Auto-Formalisation mit @HarmonicMath Aristotle des folgenden Problems der allgemeinen Gruppentheorie abgeschlossen. Fixiere drei positive ganze Zahlen n, k, m. Beweise, dass eine Untergruppe H von S_{6+(n+k+m)}, die erzeugt wird durch 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]>; H = S_{6+(n+k+m)} oder H = A_{6+(n+k+m)} erfüllt. Wir haben H = S_{6+n+k+m}, wenn und nur wenn mindestens eine der Zahlen n, k, m gerade ist, andernfalls ist H=A_{6+(n+k+m)}. GitHub-Repo mit Lean-Code und informellem Entwurf von ChatGPT-5.1-Pro. Die Auto-Formalisation in zwei gemischten Durchläufen (insgesamt etwa 20 Stunden). Der Code umfasst etwa 2600 Zeilen Lean-Code. Der Satz kann nicht mit klassischen Computer-Algebra-Systemen gelöst werden. Er umfasst den vorherigen Versuch mit den Wahlmöglichkeiten n=m=k=2, der zuvor durchgeführt wurde.