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, dass die Einteilung in unterdrückbare oder wichtige Details nicht universell ist. Hinzu kommen Seitenzahlbeschränkungen von den Herausgebern der Fachzeitschriften, die eine Konzentration auf wenige Details geradezu erzwingen.
So wie jeder Studierende wohl das stundenlange Brüten über einer Stelle im Vorlesungsskript kennt, an der zu schnell argumentiert wird (wo also Details fehlen), müssen sich Doktoranden darauf einstellen, an einem Zeitschriftartikel auch mal eine Woche zu verbringen, wenn es um das genaue Nachvollziehen der Argumentation geht. Bei Gutachtern von Artikeln sieht das natürlich nicht anders aus, sofern deren Versiertheit im Detailauffüllen nicht zur Detailunterdrückung des Autors passt. Da die Gutachtertätigkeit darüberhinaus ehrenamtlich neben den sonstigen Forschungs- und Lehraufgaben stattfindet, kann man sich vorstellen, dass eine penible Überprüfung der Korrektheit aller Beweise unrealistisch ist. Und so passiert es dann, dass in einem Gutachterbericht über eine eingereichte Arbeit der Satz "Ich glaube, der Beweis ist falsch" steht, ohne dass ein Fehler präzise benannt wird. Dass viele Gutachter auch mal "Ich glaube, der Beweis ist richtig" denken, lässt sich an vielen falschen Resultaten in der Fachliteratur belegen.
Die gängige Praxis führt damit zu einem schwer auflösbaren Konflikt: Einerseits sollen Beweise korrekt und die resultierenden Aussagen wahr sein, andererseits wünscht sich jeder Leser einen Detailgrad in der Argumentation, der auf den persönlichen Kenntnisstand abgestimmt ist.
Da eine Lösung dieses Konflikts mit klassischen statischen Texten nur schwer vorstellbar ist, soll im Projekt $\mmath$ untersucht werden, ob sich Argumentationen durch einen hierarchischen Aufbau und eine daran angepasste Darstellung in einem dynamischen Text so präsentieren lassen, dass die Leser durch tieferes Hineinklicken in den Beweis ihre gewünschte Detailgenauigkeit selbst herstellen können, während gleichzeitig eine maschinelle Überprüfbarkeit in höchster Genauigkeitsstufe möglich ist.
