Die Formalisierung mathematischer Beweise befasst sich damit, von Menschen verfasste mathematische Aussagen in ein präzises, formales Sprachsystem zu übersetzen. Damit lassen sich mittels Computern mathematische Beweise auf ihre Richtigkeit überprüfen. Die Übertragung mathematischer Aussagen in formale Sprache ist jedoch ein aufwendiger Prozess, der tiefes Verständnis sowohl der zugrunde liegenden Mathematik, als auch des jeweiligen formalen Systems erfordert. Softwaresysteme, die diesen Prozess unterstützen, werden als Beweisassistenten bezeichnet.
In den letzten Jahren hat das Gebiet bemerkenswerte Fortschritte gemacht, nicht zuletzt, weil prominente Mathematiker wie Terence Tao und Peter Scholze Beweisassistenten aktiv in ihre Arbeit einbinden und damit das Interesse einer breiteren Fachöffentlichkeit wecken. Auch die Beweisassistenten selbst sind in den letzten Jahren deutlich leistungsfähiger und zugänglicher geworden. Gleichzeitig eröffnen KI-Systeme neue Möglichkeiten, den Formalisierungsprozess teilweise zu automatisieren.
