Zwei Bonner Mathematiker erhalten 6,4 Millionen Euro vom Europäischen Forschungsrat, um mathematische Beweise künftig durch Computer überprüfen zu lassen. Christoph Thiele und Floris van Doorn von der Universität Bonn wollen mit dem Projekt HALF in den nächsten sechs Jahren grundlegende Probleme der harmonischen Analyse erforschen und diese in der Programmiersprache Lean formalisieren, wie die Hochschule mitteilte.
Laut Thiele ist es zwar prinzipiell möglich, mathematische Beweise so aufzubereiten, dass Computer sie verifizieren können, aber der Aufwand sei bei Forschungsergebnissen noch zu hoch.
Das Projekt soll dazu beitragen, diesen Prozess zu beschleunigen und zu vereinfachen. Van Doorn betonte, dass solche Formaliserungen auch für künftige KI-Anwendungen wichtig seien, um automatisch generierte Beweise überprüfen zu können.
Bereits im vergangenen Jahr hatten die Forscher in einem Pilotprojekt erfolgreich ein neues Ergebnis der harmonischen Analyse sowie einen klassischen Beweis aus dem Jahr 1966 formalisiert. Für HALF sind nun feste Stellen in der Forschungsgruppe vorgesehen, nachdem das Pilotprojekt noch mithilfe freiwilliger Helfer aus der internationalen Lean-Community umgesetzt werden konnte. (dts Nachrichtenagentur)