Ob ein mathematischer Beweis korrekt ist oder nicht, lässt sich prinzipiell maschinell überprüfen, weil die zulässigen Argumentationsmöglichkeiten präzise geregelt sind. Im einfachsten Fall müssen dafür aber alle Beweisschritte in einer festen syntaktischen Form angegeben werden, was wiederum für menschliche Leser sehr unangenehm ist: Niemand will sich einen Text in sperriger Sprache durchlesen, in dem der entscheidende argumentative Schritt zwischen einem Wust von anderen Details verschwindet.
Da versierte Leser in der Lage sind, typische argumentative Lücken schnell gedanklich auszufüllen, beschränken sich Beweistexte in der Praxis auf die Details, welche neue Techniken, Tricks und Ideen beinhalten. Die Übermittlung solcher Neuheiten ist dabei ein wichtiges Ziel mathematischer Kommunikation.
In Kombination mit einer immer stärkeren Aufspaltung der Mathematik in Spezialgebiete ergibt sich allerdings die Schwierigkeit, Read more…