Vor Kurzem bin ich auf einen sehr interesssanten Artikel gestoßen, der einen populärwissenschaftlichen Überblück zu den Versuchen in der Mathematik gibt, Beweise automatisiert prüfen zu lassen (Bischoff 2025). “Die moderne Mathematik” heißt es in dem Artikel, sei “so spezialisiert, dass selbst Experten einander nicht mehr verstehen”. Um dem Abhilfe zu schaffen, versuchen einige Forscher seit einigen Jahren, die Einführung automatischer Beweissysteme als Grundlage moderner mathematischer Forschung zu etablieren. Während diese Versuche lange Zeit wenig Beachtung fanden, scheint sich mit neueren Erfolgen, von denen Bischoff auch im Detail berichtet, allmählich ein Forschungskreis zu bilden, der automatische Beweisführung ernst nimmt und trotz der großen Widerstände, die vom Spott traditionell orientierter Kollegen bis zur riesigen Varianz von Beweisführungen aufgrund fehlender Standards reichen.
Inzwischen scheint es tatsächlich erste Programme zu geben, die erfolgreich verschiedene Beweise formalisieren und überprüfen konnten, auch wenn es anscheinend als sehr aufwendig herausgestellt hat, einzelne Beweise von den Axiomen ausgehend formal zu verfassen (ibid.). Obwohl ein Großteil der Forschung in der Mathematik nach wie vor manuell durchgeführt wird, mehren sich daher vor allem in letzter Zeit die Beispiele, wo automatisierte Beweisführung oder die explizite Zuhilfenahme von Computern vermehrt zu Erfolgen oder neuen Einsichten geführt haben.
Während es mich schon lange überrascht, dass die automatische Beweisführung in der Mathematik nicht schon längst viel weiter verbreitet ist (List 2020), befing mich beim weiteren Lesen des Textes diesmal ein komisches Gefühl von von déjà vu. Ich kenne diese menschlichen und technischen Probleme, die das Entwickeln von automatisierten Methoden zur Beweisführung mit sich bringt, nämlich nur allzu gut aus meiner eigenen täglichen Arbeit.
Denn in der historischen Linguistik ist die Situation am Ende gar nicht so unterschiedlich zur Mathematik. Wir haben scheinbar formale Methoden, die wir scheinbar formal anwenden, um zu erkennen, welche Sprachen miteinander verwandt sind und wie sich die Lautsysteme von den Ursprachen in die Tochtersprachen entwickelt haben. Diese Methoden werden jedoch nicht von Computern gegengeprüft, sondern von den jeweiligen Experten individuell angewandt und dann zu Papier gebracht. Um zu prüfen, ob die Lautwandelprozesse und die Protoformen, die jemand für eine Sprachfamilie postuliert, stimmen, muss man sich in mühseliger Kleinstarbeit zunächst in alle formalen und zuweilen auch nicht formalen Argumente einlesen, die zur Rekonstruktion der Sprachfamilie gemacht wurden. Dazu muss man die Argumente vorangegangener Arbeiten kennen, und am besten auch ein relativ gutes passives Verständnis zumindest einiger Sprachen der Sprachfamilie vorweisen können.
Bei mehr als 300 Sprachfamilien, die bisher identifiziert worden sind, haben wir auch in der Linguistik schon lange eine Situation erreicht, wo die Experten, die an unterschiedlichen Sprachfamilien arbeiten — und zuweilen sogar die Experten, die an denselben Sprachfamilien arbeiten — einander kaum noch verstehen.
Während das Problem, welches intuitive Einblicke in der historischen Linguistik spielen, mir schon lange bekannt war, und zuweilen sogar in der Literatur diskutiert worden ist (Schwink 1991: 29), hatte ich von der Mathematik jedoch bisher einen ganz anderen Eindruck gehabt. Ich war immer davon ausgegangen, dass Beweise keine Fehler aufweisen und aufgrund der formalen Ausrichtung der Mathematik mit ihren Axiomen und Formeln eine Automatisierung derselben eigentlich gar nicht so schwer sein könnte.
Dies scheint allerdings viel weniger der Fall zu sein, als ich angenommen hatte. Genauso wie in der Linguistik, wo ich relativ häufig offen angegangen werde, dass meine Versuche, die Methoden der Rekonstruktion zu automatisieren eine reine Zeitverschwendung seien, scheint das Formalisieren von Beweisen in der Mathematik mit Hilfe von Computern ebenfalls so “mühsam [zu sein], dass es in den Augen vieler Fachvertreter den Aufwand nicht lohnt” (Hartnett 2016: 61). Darüber hinaus scheint es auch in der Mathematik zuweilen zu menscheln, wenn es um die Akzeptanz von Theoremen oder Beweisen geht geht: “in the end, it is a social process that determines whether mathematicians feel confident about a theorem” (De Millo et al. 1979: 171).
Als ich vor Kurzem mal wieder eine größere Konferenz zur historischen Linguistik besuchte, wurde ich wieder auf eindrucksvolle Art und Weise damit konfrontiert, wie sehr unser Fach noch immer menschelt, ohne dass diese sozialen — und meiner Ansicht nach auch oft einfach unwissenschaftlichen Aspekte, die zur Akzeptanz oder Ablehnung von Theorien führen — wirklich ausreichend thematisiert werden. Dabei finde ich es immer wieder erschütternd, wie grob und unsachlich manche Kolleginnen und Kollegen dabei vorgehen. Da wird das Rekonstruktionssystem einer Sprachfamilie eines Kollegen A von einem Kollegen B vollständig abgelehnt, weil die Arbeit “komplett falsch” sei, obwohl sich bei einer Betrachtung der Arbeiten von A und B zeigt, dass sie sich in den meisten Fällen eigentlich nicht stark voneinander unterscheiden. Da reden die Kollegen, die zu denselben Sprachfamilien forschen, prinzipiell nicht miteinander, weil sie sich als Konkurrenz in einem Feld, das kleiner nicht sein könnte, ansehen, anstatt die Chance der Kollaboration zu ergreifen. Da werden automatisierte Lösungen, die den Vorgang der Rekonstruktion unterstützen und seine Transparenz erhöhen können, pauschal und ohne Begründung abgelehnt, weil man der eigenen Intuition ja ohnehin mehr vertraue.
Während ich, wenn man mich mit der typischen Kritik an computergestützten Methoden konfrontiert, meist gute Miene zu einem Spiel mache, das ich inzwischen nur zu gut kenne, obwohl es mich schon lange nervt, wundert es mich doch immer wieder, mit welch unwissenschaftlichen Argumenten jegliche Bezugnahme auf Computer abgelehnt wird. Vor allem stört es mich, dass sich vor allem die lautesten Kritiker eigentlich kaum die Mühe geben, sich überhaupt mit den Lösungen, welche die Tools, die ich entwickle bieten, grundlegend vertraut zu machen.
Die meisten vermuten in Tools wie der EDICTOR-Software (https://edictor.org, List et al. 2025) schlicht den Versuch, alle manuellen Schritte des Sprachvergleichs komplett zu automatisieren und werfen der Software dann vor, im Gegensatz zum Menschen schlechtere Ergebnisse zu liefern. Dabei geht es gar nicht um die Automatisierung des historischen Sprachvergleichs, sondern um die Steigerung seiner Transparenz und Wiederholbarkeit. Wer sich aktuelle Rekonstruktionen von unterschiedlichen Sprachfamilien wie der Mataco-Sprachen in Südamerika (Nikulin und Carlo 2024), der Tschadischen Sprachen in Afrika (Wolff 2022) oder der Sogeram-Sprachen in Neuginea (Daniels 2020) anschaut, wird feststellen, dass es kaum Gemeinsamkeiten in Bezug auf die Präsentation der Daten oder der Methoden, mit deren Hilfe die Daten erstellt wurden, gibt. Einzelne Rekonstruktionen von individuellen kognaten Wörtern in den Sprachfamilien werden zwar in allen Fällen mitsamt der Reflexe, also der Belegwörter in den Einzelsprachen aufgelistet, man wird jedoch nahezu komplett allein gelassen, wenn man die Belege mit den Rekonstrukten in Beziehung setzen möchte.
Obwohl wir von formalen Prozeduren, wie der Sequenzalinierung (List 2014) oder der Inferenz von Korrespondenzmustern (List 2019) ausgehen, ohne deren Hilfe die Wortvergleiche gar nicht aufgestellt werden könnten, finden wir diese in den Ergebnissen, die präsentiert werden, eigentlich nie vor. Auch werden die Rohdaten, die die Autoren nutzen, um ihre Rekonstruktionen zu erstellen, eigentlich so gut wie nie geteilt. Wer diese also nachvollziehen oder auf ihne aufbauen will, muss zunächst die Daten digitalisieren und dann die Methoden unabhängig neu anwenden. Wissenschaft sollte eigentlich nach höherer Transparenz, Nachvollziehbarkeit und Wiederholbarkeit streben, vor allem, wenn man erwartet, dass sie ernst genommen wird.
Wenn ich Kollegen darauf hinweise, dass die Transparenz von Daten wichtig ist, um deren Weiterbearbeitung zu ermöglichen, ernte ich in vielen Fällen nur verständnislose Blicke. Zuweilen haben mir Kollegen sogar direkt gesagt, dass ihnen die Nachnutzung ihrer Arbeit eigentlich egal sei. Wenn sich Forschung aber nur auf die eigenen Interessen derer, die forschen, konzentriert und das Aufbereiten von Wissen und Erkenntnissen für die Nachnutzung vollständig ignoriert, dann verkommt sie zu einem komischen Selbstzweck, der überspitzt gesagt am Ende eigentlich nur einigen privilegierten Menschen die Ausübung ihrer Hobbies in ihrer Arbeitszeit finanziert.
Ich habe jedoch eine gewisse Hoffnung, dass sich das — wenn auch langsamer als in der Mathematik — auch in der Linguistik allmählich ändern wird. Jüngere Menschen, die Linguistik betreiben, haben schon heute weitaus bessere Computerkenntnisse als die Generationen vor ihnen. Da computergestützte Ansätze und transparente Verfahren entgegen der Vorurteile, die einige Linguisten ihnen noch immer entgegenbringen, die konkrete Forschungsarbeit tatsächlich nicht nur transparenter, sondern auch effizienter gestalten können, besteht Hoffnung, dass wir von einem Fach mit wenigen Experten, die sich als Platzhirsche gerieren, zu einem Fach werden, in dem die wenigen Experten mehr Zeit haben, die spezifischen Probleme ihrer Vergleichsstudien im Team anzugehen.
Literatur
Bischoff, Manon Was passiert, wenn niemand mehr die Mathematik versteht? Spektrum — Die Woche 2025.33. 21-35. https://www.spektrum.de/news/so-veraendern-computer-ki-und-beweispruefer-die-mathematik/2280992
Daniels, Don (2020): Grammatical reconstruction. The Sogeram languages of New Guinea. Boston and Berlin: De Gruyter Mouton.
De Millo, Richard A. and Lipton, Richard J. and Perlis, Alan J. (1979): Social processes and proofs of theorems and programs. Communications of the ACM 22.5. 271-280.
List, Johann-Mattis and van Dam, Kellen Parker and Blum, Frederic (2025): EDICTOR 3. An Interactive Tool for Computer-Assisted Language Comparison [Software Tool, Version 3.1]. Passau: MCL Chair at the University of Passau. https://edictor.org
Hartnett, Kevin (2016): Werden Computer das Wesen der Mathematik verändern? Spektrum der Wissenschaft 12. https://www.spektrum.de/magazin/werden-computer-das-wesen-der-mathematik-veraendern/1427414
List, Johann-Mattis (2014): Sequence comparison in historical linguistics. Düsseldorf: Düsseldorf University Press. https://sequencecomparison.github.io
List, Johann-Mattis (2019): Automatic inference of sound correspondence patterns across multiple languages. Computational Linguistics 45.1. 137-161. https://doi.org/10.1162/COLI_a_00344
List, Johann-Mattis (2020): Von Handarbeit im digitalen Zeitalter [Of manual work in the digital age]. Von Wörtern und Bäumen 4.9. https://doi.org/10.58079/vbqp
Nikulin, Andrey and Carol, Javier (2024): Historical phonology of Mataguayan. Berlin: Language Science Press.
Schwink, Frederick (1991): Linguistic typology, universality and the realism of reconstruction. Washington: Institute for the Study of Man.
Wolff, H. Ekkehard (2022): A historical phonology of Central Chadic. Prosodies and lexical reconstruction. Cambridge: Cambridge University Press.