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
| 10.10.2022 | Workshop zu Lean AI (232 im MI, 9.30-12.00) |
| 19.09.2022 | Workshop zu Lean AI an der Universität Freiburg (232 im MI, 9.30-16.00) |
| 7.07.2022 | Das Projekt LeanAI wird von der Vector-Stiftug im Programm MINT-Innovationen 2022 gefördert. |
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.