Für diejenigen, die sich fragen, die betreffende KI war eine Testversion von Aristotle von @HarmonicMath. Der Satz war ein Ergebnis der letzten Meile über Summen von Reihen, das benötigt wurde, um einen Algorithmus für wissenschaftliches Rechnen in einem domänenspezifischen Verifier zu verifizieren, der von meinem Forschungsteam in Lean entwickelt wurde.