Beyond High School: Proof, Olympiad Training, and PhD-Level Mathematics — What "PhD Mode" Could Realistically Contain

Ergebnisse

(a) Der Übergang‑zu‑Beweis‑Kurs und Forschung zum Lehren von Beweisen

Die meisten US‑Abteilungen bieten zwischen Analysis und dem ersten stark beweisorientierten Kurs (Algebra, reelle Analysis) einen „Transition‑to‑Proof“-Kurs an [1]. Die vorherrschende Didaktik ist die Moore‑Methode: Der Dozent gibt nur Axiome und eine sequenzierte Aufgabenliste vor; die Studierenden dürfen keine Lehrbücher konsultieren, alles selbst beweisen und einander präsentieren [1][2]. Evidenz für die Wirksamkeit ist überwiegend qualitativ und langfristig (mehr Studierende gehen in die Forschung) und nicht streng quantitativ [2].

Die Forschung von Selden & Selden zieht eine für die Bewertungs­gestaltung zentrale Unterscheidung: Beweiskonstruktion und Beweisvalidierung (Beurteilung, ob das Argument einer anderen Person korrekt ist) sind separate Kompetenzen, und ein auf Konstruktion ausgerichteter Kurs verbessert die Validierung nicht zuverlässig [3][4]. Eye‑Tracking‑ und Think‑Aloud‑Studien zeigen, dass Anfängerinnen sich auf Oberflächenmerkmale (algebraische Manipulation) fixieren, während Expertinnen die globale logische Struktur verfolgen; Validierung wird als aktives Sinn‑machen formuliert, nicht als binäre Prüfung – genau deshalb widersteht sie einer maschinell angewandten Rubrik [3][4].

Der Umgang mit Quantoren ist das am häufigsten replizierte Schwachstellenfeld: Eine Studie mit 61 Studierenden ergab, dass keiner konsequent eine informelle Behauptung in ihr korrektes formales, quantifiziertes Äquivalent umschreiben konnte [1]. Wiederkehrende Fehlermodi: Keine Variable einführen beim Beweis einer universellen Aussage; Eigenschaften übermäßig einem existenziellen Zeugen zuschreiben; die Quantorenreihenfolge vertauschen (klassisch in ε‑δ‑Beweisen); und eine Aussage falsch negieren (die „Gegenseite“ angeben statt die logische Negation), was den Beweis per Widerspruch untergräbt [5][6]. Eine lineare‑Algebra‑Studie fand ähnlich, dass Studierende „aneinander vorbeisprachen“ wegen unterschiedlicher Bedeutungen von „einzigartig“ [6]. Dies sind diskrete, klar definierte Fehlermodi – jeder lässt sich durch eine enge, prüfbare Übung adressieren (siehe Design Implications).

(b) Wie Olympiade‑Training funktioniert

Olympiade‑Training ist um Heuristiken + einen Techniken‑Bank strukturiert, nicht um einen linearen Lehrplan. Pólyas How to Solve It (1945) liefert die vierstufige Heuristik – verstehen, planen, ausführen, zurückblicken – die im Wesentlichen allen Wettbewerbs‑Trainings‑Literaturen zugrunde liegt [7][11]. Engels Problem‑Solving Strategies (Springer, 1998), das sich an Trainer bis zum IMO/Putnam‑Niveau richtet, ordnet nach Techniken (Invarianten, Schubladenprinzip, Extremalprinzip, Induktion, Färben/Zählen) statt nach MSC‑Fächern [10][11].

AoPS operationalisiert dies in großem Maßstab – Aufgaben vor Erklärungen, Lehrpläne von Pre‑Algebra bis MATHCOUNTS/AMC/AIME/ARML und WOOT (Olympiade‑Training); jedes US‑IMO‑Teammitglied seit 2015 war ein AoPS‑Student [8]. Die Putnam‑Vorbereitung folgt demselben auf Aufgaben‑Sätzen basierenden Modell, verstärkt durch seminarartige Gruppensitzungen [9][11].

Die Bewertung in beiden ist bewusst grob und nicht‑additiv – eine Ablehnung der Punkte‑pro‑Schritt‑Bewertung. IMO‑Aufgaben werden mit 0‑7 Punkten bewertet, entweder „von 7 abwärts“ (nahezu vollständig) oder „von 0 aufwärts“ (fehlende kritische Idee); Teilpunkte spiegeln konzeptuellen Fortschritt wider, nicht die Zeilenzahl [23][24]. Putnam verwendet 0‑10, vergibt aber praktisch nur {0,1,2,8,9,10} – die „Gap of Death“ (3‑7) wird fast nie genutzt, sodass ein Beweis, dem die volle Strenge fehlt, ≤2 Punkte erhält, unabhängig von sonst korrekt erscheinender Arbeit [12]. Das ist ein klares Signal, dass menschlich bewertete Teilpunkte bei Beweisen jedem additiven, mechanischen Rubrikmodell widerstehen – dieselbe Lücke, die automatisierte Bewertungs‑Systeme noch nicht schließen können (Teil d).

(c) Die Themen‑Taxonomie der fortgeschrittenen Mathematik und PhD‑Qualifikationsprüfungen

Die Mathematics Subject Classification (MSC 2020), gemeinsam gepflegt von AMS/MathSciNet und zbMATH, ist das dem offiziellen Taxonomie‑System aller Mathematik am nächsten kommende System: 63 zweistellige Top‑Level‑Codes, von 00 General und 03 Logik über die Algebra‑Familie (12‑20), die Analyse/Geometrie/Topologie‑Familie (26‑58), Wahrscheinlichkeit/Statistik (60‑62), angewandte Bereiche (68 CS, 76‑86 Mechanik, 90‑94 OR/Spieltheorie/Information) bis zu 97 Mathematikdidaktik [15][16]. Jeder Code unterteilt sich in buchstabierte Zweitebene‑Gebiete [15].

PhD‑Qualifikationsprüfungen ziehen ein kleines, relativ universelles Kernset statt der vollen 63 Bereiche heran. Harvard nennt sechs: Algebra (Sylow, Ringe/Moduln, Galois, Darstellungstheorie), Algebraische Geometrie (Varietäten, Riemann‑Roch), Komplexe Analysis (Cauchy‑Theorie, Residuen, Riemann‑Flächen), Algebraische Topologie (Fundamentalgruppe, (Ko)Homologie, Poincaré‑Dualität), Differentialgeometrie (Mannigfaltigkeiten, Bündel, Krümmung) und Reelle Analysis (Maßtheorie, Lp‑Räume, Fourier‑Analyse, PDEs, Wahrscheinlichkeit, Sobolev‑Räume) [13]. Andere Hochschulen (TCU, UNT, Stanford, Penn State) verlangen 2‑4 Prüfungen aus einem ähnlichen, kleineren Angebot – was bestätigt, dass „PhD‑Level“ Tiefe in einer Handvoll Kernpfeilern bedeutet, nicht eine enzyklopädische MSC‑Abdeckung [14].

(d) Automatisch bewertbare Formate für fortgeschrittene Mathematik

STACK (Moodle, unterstützt vom Maxima‑CAS) und WeBWorK (Perl‑basierte „PG“-Sprache) sind die beiden ausgereiften, weit verbreiteten Systeme für numerische/symbolische Antwortprüfung: beide validieren Eingaben, prüfen algebraische Äquivalenz (nicht String‑Match) mittels zufälliger pro‑Student‑Parameter und geben sofortiges Feedback – keines von beiden behauptet, einen schriftlichen Beweis zu bewerten [17][18][19]. Die gleiche Technik – subtrahieren, vereinfachen, prüfen, ob das Residuum symbolisch Null ist, oder auf numerische Auswertung zurückgreifen – wird von SymPy‑artigen Bibliotheken programmatisch bereitgestellt und liegt den modernen Math‑LLM‑Bewertungs‑Frameworks zugrunde [25].

Für die tatsächliche Beweis‑Bewertung ist der einzige mechanisch solide Ansatz ein Beweisassistent: Lean 4 + mathlib kompiliert einen Beweis und akzeptiert oder verwirft ihn – kein Teilpunkt, aber keinerlei Mehrdeutigkeit [20]. Das Natural Number Game (Imperial College London) zeigt, dass dies als Lehrprodukt funktioniert, indem es die Peano‑Axiome spielerisch macht, sodass „offensichtliche“ Fakten wie a+b=b+a einem Compiler bewiesen werden müssen; „Mathematics in Lean“ erweitert die Idee auf Inhalte für das Grundstudium [20][21].

Die Bewertung von **natürlichen Sprach‑**Beweisen – dem Format, das Studierende tatsächlich schreiben – bleibt ungelöst. LeanTutor (2026) autoformalisiert einen Beweis schrittweise in Lean, benötigt jedoch eine bereits vorhandene formalisiert­e Lösung des Lehrpersonals [26]. IMO‑GradingBench (2025), basierend auf 1.000 von Menschen bewerteten IMO‑Lösungen, ergab, dass selbst modernste Modelle (o3, Gemini 2.5 Deep Think) nur 52‑54 % exakte Übereinstimmung mit menschlichen Bewertern blind (ohne Referenz) erreichen, wobei Fehler vor allem beim Unterscheiden von „teilweise“ und „falsch“ auftreten; Menschen mit Referenz korrelieren bei 0,96 [22]. RefGrader (2025) erhöht die Zuverlässigkeit, indem stets gegen eine Referenz bewertet wird statt blind, was jedoch voraussetzt, dass diese Referenz vorab erstellt ist [27]. Die Bewertung von Beweisen in natürlicher Sprache durch KI ist real, aber zu unzuverlässig an der schwierigsten Grenze, um das alleinige Bewertungs‑Mechanismus für sofortiges, vertrauenswürdiges Feedback zu sein.

Designimplikationen für Math Challenge

Vorgeschlagene Bänder über der Oberstufe, jedes mit konkreten Themen und – entscheidend – einem ehrlichen, realistischen automatischen Bewertungssystem:

1. Band U1 — Übergang zum Beweis. Themen: Aussagen‑/Prädikatenlogik, Quantoren‑Manipulation (∀/∃‑Reihenfolge, Negation), direkter Beweis, Kontraposition, Induktion, Beweis durch Widerspruch, Grundbegriffe der Mengenlehre und Funktionen. Automatische Bewertung: Multiple‑Choice/Mehrfachauswahl zu „welche dieser Negationen ist korrekt“, „füge den fehlenden Quantor ein“ und Schritt‑Reihenfolge‑Übungen (Zeilen eines gültigen Beweises mischen, Lernende ordnen sie neu) — dies zielt direkt auf die dokumentierten Quantoren‑ und Strukturfehler von Selden & Selden sowie die Quantoren‑Reihen‑Literatur [3][5][6] ab.

2. Band U2 — Beweisvalidierung als eigenständige Fähigkeit. Präsentieren Sie einen kurzen „Beweis“ mit einem eingebetteten Fehler (falsche Quantoren‑Reihenfolge, unbegründeter Schritt, zirkuläres Schließen) und lassen Sie die Lernenden die exakte Zeile auswählen, die bricht, oder das gesamte Argument als gültig/ungültig/unvollständig klassifizieren. Dies ist direkt motiviert durch Selden & Selden’s Befund, dass Übung im Konstruieren nicht automatisch auf Validierungsfähigkeit überträgt — sie benötigt einen eigenen Aufgabentyp [3][4].

3. Band U3 — Abstrakte Algebra (Gruppen, Ringe, Körper). Themen: Gruppenaxiome, Lagrange‑Satz, zyklische Gruppen, Homomorphismen/Isomorphismen, Quotientengruppen, Grundbegriffe der Ring‑/Körpertheorie. Automatische Bewertung: numerische/strukturelle Antworten (Ordnung eines Elements, ist diese Abbildung ein Homomorphismus — Ja/Nein mit erforderlichem Gegenbeispiel, falls Nein), Ausfüllen von Cayley‑Tabellen, Multiple‑Choice zu „welches Axiom hier fehlt“.

4. Band U4 — Reelle Analysis. Themen: Folgen/Grenzwerte, ε‑δ‑Stetigkeit, Differenzierbarkeit, Riemann‑Integration, Konvergenztests für Reihen. Automatische Bewertung: numerische Antwort (Finde N, sodass |a_n − L| < ε), Multiple‑Choice zu welchem Konvergenztest anzuwenden ist, und Gegenbeispiel‑Eingabe („gib eine Folge an, die punktweise, aber nicht gleichmäßig konvergiert“) — geprüft gegen eine Bibliothek bekannter gültiger Gegenbeispiele plus einen symbolisch/numerischen Verifizierer (Auswertung des Kandidaten an Stichprobenpunkten).

5. Band U5 — Lineare Algebra über den Einführungs‑Kurs hinaus. Themen: Eigenwerte/Eigenvektoren, Diagonalisierung, Jordan‑Normalform, Skalarprodukte, Spektralsatz. Automatische Bewertung: vollständig numerisch/symbolisch — dieses Band ist im Wesentlichen frei mit einem SymPy‑äquivalenten CAS‑Backend (das STACK/Maxima‑Modell lässt sich fast direkt übernehmen) [17][18].

6. Band U6 — Kombinatorik & Zahlentheorie (olympiadisch). Themen: Schubfachprinzip, Invarianten, modulare Arithmetik, erzeugende Funktionen, extremale Kombinatorik — direkt modelliert nach Engels Taxonomie und AoPS/WOOT‑Struktur [8][10]. Automatische Bewertung: dieses Band passt am besten zum bestehenden Modell von Math Challenge — nahezu alle Aufgaben besitzen eine einzige numerische oder geschlossene Endantwort, exakt wie AMC/AIME/Putnam‑Stil Lückentexte, sodass keine neue Bewertungsmechanik über das bereits vorhandene Ladder‑System hinaus nötig ist.

7. Band G1 — Topologie. Themen: metrische/topologische Räume, Kompaktheit, Zusammenhang, Stetigkeit, Grundlagen der Fundamentalgruppe. Automatische Bewertung: Multiple‑Choice („ist dieser Raum kompakt — Ja/Nein, wähle die überdeckende Menge, die scheitert“), Wahr/Falsch mit Auswahl einer Begründung (wähle die von 4 Kandidaten gültige Begründung), da offene topologische Beweise ohne Formalisierung nicht mechanisch prüfbar sind.

8. Band G2 — Maßtheorie & fortgeschrittene reelle Analysis. Themen: σ‑Algebren, Lebesgue‑Maß, messbare Funktionen, L^p‑Räume, dominierter Konvergenzsatz. Automatische Bewertung: überwiegend numerisch (berechne ein Lebesgue‑Integral, bestimme, ob eine Funktion zu L^p gehört) plus Multiple‑Choice, welcher Konvergenzsatz auf ein gegebenes Szenario zutrifft — eine nahezu direkte Abbildung des Qualifikations‑Syllabus für reelle Analysis an der Harvard‑Universität [13].

9. Band G3 — Komplexe Analysis. Themen: Holomorphie, Cauchy‑Satz, Residuen, konforme Abbildungen, Riemann‑Abbildungssatz. Automatische Bewertung: numerisch (wertet ein Konturintegral mittels Residuen aus — klassische CAS‑prüfbare Aufgabe) plus Multiple‑Choice zur Klassifikation von Singularitäten.

10. Band G4 — Algebraische Topologie / Differentialgeometrie. Themen: Homologie/Kohomologie‑Berechnung für Standardräume (Kugeln, Tori, projektive Räume), Krümmung standardisierter Flächen. Automatische Bewertung: numerisch (Betti‑Zahlen, Euler‑Charakteristik) — berechenbar und prüfbar — aber echter Beweisinhalt (z. B. „beweise Poincaré‑Dualität für diesen Raum“) ist nicht automatisch bewertbar und sollte als rein lesbares „ausgearbeitetes Beispiel“ bereitgestellt werden, nicht als bewertete Herausforderung.

11. Band PhD‑1 — PDEs & Wahrscheinlichkeit (Kern des Qualifikations‑Examen). Themen: Wärme‑/Wellen‑/Laplace‑Gleichungen, schwache Lösungen, Grundlagen der Sobolev‑Einbettungen; maßtheoretische Wahrscheinlichkeit, charakteristische Funktionen, Zentraler Grenzwertsatz. Automatische Bewertung: numerische Lösungskontrolle für kanonische PDEs (prüfe, ob eine Kandidatenlösung die PDE und Randbedingungen durch direkte Substitution erfüllt — rein mechanisch und CAS‑freundlich) und Fragen zur Wahrscheinlichkeitsberechnung.

12. Band PhD‑Lean — „Formell verifiziert“ Capstone‑Track, klar gekennzeichnet als anders als die übrigen. Themen: eine kuratierte Sequenz kleiner Lemmas (im Geiste des Natural Number Game) hin zu einem nichttrivialen Resultat, erstellt in Lean 4 gegen mathlib. Automatische Bewertung: Der Compiler selbst ist der Prüfer — ein Beweis wird als bestanden/fehlgeschlagen durch erfolgreiche Kompilierung bewertet, ohne Bewertungs‑Mehrdeutigkeit, jedoch zu hohen Autor*innen‑Kosten (jede Aufgabe benötigt ein Lean‑prüfbares Gerüst) und mit erheblichem Lernaufwand für die Teilnehmenden (Lean‑Syntax, nicht nur Mathematik) [20][21].

13. Explizit nicht zulässig: freiformige, natürliche‑sprachliche Beweisbewertung durch KI als bewertete (nicht tutorielle) Mechanik. Angesichts der ~52‑54 % blinden Bewertungs‑Übereinstimmung von IMO‑GradingBench mit menschlichen Juroren selbst bei Frontier‑Modellen 2025‑2026 [22] sollte Math Challenge keine Funktion bereitstellen, die studentisch geschriebene Prosa‑Beweise allein durch LLM‑Urteil mit Pass/Fail oder numerischer Punktzahl bewertet. Es ist jedoch angemessen, dass das bestehende „KI‑Tutor‑Feedback nach jeder Herausforderung“ qualitative, nicht‑bewertende Kommentare zu einem eingereichten Beweisskizze liefert (dies ist ein Coaching‑Feature, keine benotete Bewertung, sodass ein falsches oder übermütiges Urteil ein UX‑Qualitätsproblem, aber kein Integritätsproblem der Bewertung darstellt) — diese Unterscheidung (Feedback vs. Score) ist genau das, was die PhD‑Modus‑Bänder ehrlich darüber hält, was „automatisch bewertbar“ bedeutet.

14. Querschnitts‑Mechanismus: Übernahme von RefGraders Kernidee — immer gegen eine Referenz bewerten, nie blind — für jede KI‑unterstützte Bewertung im PhD‑Modus. Da referenzbasierte agentische Bewertung nachweislich blindes Bewerten übertrifft [22][27], sollte jeder Ort, an dem der Tutor offenes Schließen evaluiert (nicht nur der oben genannte No‑Go‑Fall), stets die kanonische Lösung/Rubrik als Kontext erhalten und niemals ein Beweis ohne Referenz beurteilt werden.

Offene Fragen für den Projektinhaber

1. Sollte der „PhD-Modus“ den Lean-geprüften Capstone-Track (Punkt 12) trotz seiner Erstellungskosten enthalten, oder ganz bei numerischen/Multiple-Choice-/Gegenbeispiel-Formaten bleiben?
2. Ist eine reine Coaching-Durchsicht (nicht bewertet) von KI-Beweisskizzen für die oberen Bänder akzeptabel, oder muss jede Herausforderung eine harte Bestanden/Nicht-bestanden-Bewertung liefern?
3. Sollten die Bandgrenzen strikt den MSC-Top-Level-Codes folgen (für ein Feature „nach MSC-Bereich durchsuchen“), oder um den Kern der PhD-Qualifikationsprüfung herum organisiert bleiben (der enger und pädagogisch üblicher ist)?
4. Besteht Interesse daran, eine bestehende CAS-gestützte Engine zu lizenzieren/integrieren (STACKs Maxima-Pipeline ist Open-Source und Moodle-nativ), statt numerische/symbolische Äquivalenzprüfung von Grund auf neu zu bauen?