KI widerlegt Vermutungen von Erdős und Grothendieck: Mathematiker werden von Gegenbeispielen überrollt

Human mathematicians are being outcounterexampled

In den letzten Wochen haben KI-Systeme wie ChatGPT und Claude Fable mehrere bedeutende mathematische Vermutungen widerlegt, darunter die Unit-Distance-Vermutung von Erdős und eine Frage von Grothendieck über Gruppenschemata. Die Beweise wurden teilweise in Lean formalisiert, wobei ein System 1,2 Millionen Zeilen Code generierte. Der Autor, ein Lean-Maintainer, reflektiert über die Implikationen für die mathematische Gemeinschaft und berichtet von einem weiteren Gegenbeispiel zur Jacobi-Vermutung, das Fable gefunden hat.