Lean AI

Dieses von Prof. Pfaffelhuber und Prof. Schmidt geleitete Projekt und von der Vector Stiftung geförderte Projekt beschäftigt sich mit der Verbindung von maschinellem Lernen und LEAN.

Aktuelles

Projektbeschreibung

In den letzten Jahren erzielte maschinelles Lernen in vielen Bereichen bis dato unvorstellbare Erfolge, insbesondere in der Übersetzung von Sprachen. Gleichzeitig ist unserem Freiburg Kollegen Johann Commelin der sensationelle Nachweis einer Behauptung des Fields-Medallisten Peter Scholze mit Hilfe der Theorem-Proving Software Lean gelungen.

Ziel dieses Projektes ist eine künstliche Intelligenz LeanAI zu entwickeln, die wechselseitig von Mathematik in Lean übersetzt und umgekehrt. Ein solche Möglichkeit wäre ein herausragendes Hilfsmittel für die aktuelle Forschung und deren Anwendung. Langfristig gesehen ist dies ein erster Schritt in die Richtung von  computergestützten mathematischen Beweisen bis hin zu selbständigen Beweisen mathematischer Aussagen. Dieser völlig neuartige Ansatz geht einher mit einem besonderen Risiko.