LeanAI

In den letzten Jahren erzielte maschinelles Lernen in vielen Bereichen bis dato unvorstellbare Erfolge, wie etwa bei der Sprach- und Bilderkennung, beim automatisierten Fahren, bei Schach und Go. Wieso soll es nicht auch möglich sein, Methoden der Künstlichen Intelligenz zu verwenden, um mathematische Beweise zu finden?

In diesem Projekt der Universität Freiburg soll die Open-Source Software Lean so trainiert werden, dass sie mathematische Beweisführungen überprüfen und in der Zukunft vielleicht sogar eigenständig Beweise finden kann.