Automatische Theorembeweiser sind Computerprogramme, die eine Menge von Annahmen (genannt Axiome) und eine Vermutung als Eingabe erhalten und dann innerhalb einer vorher bestimmten Zeit versuchen, vollautomatisch einen formalen (mathematischen) Beweis für die Gültigkeit der Vermutung zu finden. Dazu werden sowohl die Annahmen als auch die Vermutung in einem mathematischen Logikformalismus (z.B. Prädikatenlogik) formuliert. In der jährlich stattfindenen Weltmeisterschaft solcher Theorembeweiser (der sogenannten CADE System Competition, kurz: CASC) treten die besten Theorembeweiser in verschiedenen Kategorien gegeneinander an und versuchen, aus den 500 zufällig gewählten Problemen so viele wie möglich zu lösen. Leo-III tritt dabei in einer besonders herausfordernden Kategorie des Theorembeweisens an, bei der viele Aspekte noch Gegenstand aktueller Grundlagenforschung sind. Dennoch schaffte es der vergleichsweise junge Leo-III 382 der 500 gestellten Aufgaben
als korrekt zu beweisen; einzig der an der University of Innsbruck und Czech Technical University in Prague entwickelte Beweiser Satallax konnte mehr Beweise liefern. In weiteren Kategorien, die nicht im primären Anwendungsgebiet von Leo-III liegen, erreichte Leo-III ebenfalls solide Platzierungen.

Die Entwicklung von Leo-III wurde von der deutschen Forschungsgemeinschaft (DFG) gefördert und ist als Open Source Software frei verfügbar.
 
Links:
Leo-III Projektseite: http://www.inf.fu-berlin.de/users/lex/leo3/
Leo-III Beweiser: https://github.com/leoprover/Leo-III
Dahlem Center for Machine Learning and Robotics: http://www.mi.fu-berlin.de/inf/groups/ag-ki/index.html
CASC Weltmeisterschaft 2017: http://www.cs.miami.edu/~tptp/CASC/26/