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

Findings

(a) The transition-to-proof course and research on teaching proof

Most US departments insert a “transition to proof” course between calculus and the first proof-heavy course (algebra, real analysis) [1]. Its dominant pedagogy is the Moore method: the instructor gives only axioms and a sequenced problem list; students may not consult texts, prove everything themselves, and present to each other [1][2]. Evidence for effectiveness is mostly qualitative and long-run (more students moving into research) rather than tightly quantitative [2].

Selden & Selden’s research draws a distinction central to assessment design: proof construction and proof validation (judging whether someone else’s argument is correct) are separate competencies, and a construction-focused course does not reliably improve validation [3][4]. Eye-tracking and think-aloud studies show novices fixate on surface features (algebraic manipulation) while experts track global logical structure; validation is framed as active sense-making, not a binary check — which is exactly why it resists a machine-applied rubric [3][4].

Quantifier handling is the single most-replicated failure area: one study of 61 students found none could consistently rewrite an informal claim as its correct formal quantified equivalent [1]. Recurring failure modes: not introducing a variable when proving a universal statement; over-attributing properties to an existential witness; swapping quantifier order (classic in ε-δ proofs); and mis-negating a statement (stating the “opposite” rather than the logical negation), which undermines proof by contradiction [5][6]. A linear-algebra study similarly found students “talking past each other” over differing meanings of “unique” [6]. These are discrete, well-defined failure modes — each targetable by a narrow, checkable exercise (see Design Implications).

(b) How olympiad training works

Olympiad training is organized around heuristics + a technique bank, not a linear syllabus. Pólya’s How to Solve It (1945) supplies the four-stage heuristic — understand, plan, execute, look back — underlying essentially all competition-training literature [7][11]. Engel’s Problem-Solving Strategies (Springer, 1998), aimed at trainers up to IMO/Putnam level, organizes by technique (invariants, pigeonhole, extremal principle, induction, coloring/counting) rather than MSC subject [10][11].

AoPS operationalizes this at scale — problems before explanations, curricula from Prealgebra through MATHCOUNTS/AMC/AIME/ARML and WOOT (olympiad training); every US IMO team member since 2015 has been an AoPS student [8]. Putnam prep follows the same problem-set-driven model, reinforced by seminar-style group sessions [9][11].

Grading in both is deliberately coarse and non-additive — a rejection of point-per-step scoring. IMO problems score 0-7, graded either “from 7 down” (near-complete) or “from 0 up” (missing a critical idea); partial credit reflects conceptual progress, not line count [23][24]. Putnam uses 0-10 but effectively only awards {0,1,2,8,9,10} — the “Gap of Death” (3-7) is nearly unused, so a proof missing full rigor scores ≤2 regardless of surrounding correct-looking work [12]. This is a direct signal that human-judged partial credit on proofs resists any additive, mechanical rubric — the same gap automated graders still cannot close (part d).

(c) The topic taxonomy of advanced mathematics and PhD qualifying exams

The Mathematics Subject Classification (MSC 2020), jointly maintained by AMS/MathSciNet and zbMATH, is the closest thing to an official taxonomy of all mathematics: 63 top-level two-digit codes, from 00 General and 03 Logic through the algebra family (12-20), the analysis/geometry/topology family (26-58), probability/statistics (60-62), applied areas (68 CS, 76-86 mechanics, 90-94 OR/game theory/information), to 97 Mathematics education [15][16]. Each code subdivides into lettered second-level areas [15].

PhD qualifying exams sample a small, fairly universal core rather than the full 63 areas. Harvard names six: Algebra (Sylow, rings/modules, Galois, representation theory), Algebraic geometry (varieties, Riemann-Roch), Complex analysis (Cauchy theory, residues, Riemann surfaces), Algebraic topology (fundamental group, (co)homology, Poincaré duality), Differential geometry (manifolds, bundles, curvature), and Real analysis (measure theory, Lp spaces, Fourier analysis, PDEs, probability, Sobolev spaces) [13]. Other schools (TCU, UNT, Stanford, Penn State) require 2-4 exams from a similar, smaller menu — confirming that “PhD-level” means depth in a handful of core pillars, not encyclopedic MSC coverage [14].

(d) Auto-gradable formats for advanced math

STACK (Moodle, backed by the Maxima CAS) and WeBWorK (Perl-based “PG” language) are the two mature, widely deployed systems for numeric/symbolic answer checking: both validate input, check algebraic equivalence (not string match) via random per-student parameters, and give instant feedback — neither claims to grade a written proof [17][18][19]. The same technique — subtract, simplify, check the residual is symbolically zero, or fall back to numeric evaluation — is what SymPy-style libraries provide programmatically, and underlies contemporary math-LLM grading harnesses [25].

For actual proof grading, the only mechanically sound approach is a proof assistant: Lean 4 + mathlib compiles a proof and accepts or rejects it — no partial credit, but zero ambiguity [20]. The Natural Number Game (Imperial College London) proves this works as a teaching product, gamifying the Peano axioms so “obvious” facts like a+b=b+a must be proved to a compiler; “Mathematics in Lean” extends the idea to undergraduate content [20][21].

Grading natural-language proofs — the format students actually write — remains unsolved. LeanTutor (2026) autoformalizes a proof step-by-step into Lean, but needs a pre-existing formalized staff solution [26]. IMO-GradingBench (2025), from 1,000 human-graded IMO solutions, found even frontier models (o3, Gemini 2.5 Deep Think) reach only 52-54% exact agreement with human graders blind (no reference), with errors concentrated in distinguishing “partial” from “wrong”; humans with a reference correlate at 0.96 [22]. RefGrader (2025) improves reliability by always grading against a reference rather than blind, at the cost of needing that reference pre-built [27]. Natural-language proof grading by AI is real but too unreliable at the hardest boundary to be the sole grading mechanism for instant, trustworthy feedback.

Design implications for Math Challenge

Proposed bands above high school, each with concrete topics and — critically — an honest, realistic auto-grading mechanism:

1. Band U1 — Transition to Proof. Topics: propositional/predicate logic, quantifier manipulation (∀/∃ order, negation), direct proof, contrapositive, induction, proof by contradiction, basic set theory and functions. Auto-grading: multiple-choice/multi-select on “which of these is the correct negation of this statement,” “insert the missing quantifier,” and step-ordering exercises (shuffle a valid proof’s lines, student reorders them) — this directly targets the documented quantifier and structure failures from Selden & Selden and the quantifier-order literature [3][5][6].

2. Band U2 — Proof validation as its own skill. Present a short “proof” with a seeded flaw (wrong quantifier order, unjustified step, circular reasoning) and ask the student to select the exact line that breaks, or classify the whole argument as valid/invalid/incomplete. This is directly motivated by Selden & Selden’s finding that construction practice does not transfer to validation ability — it needs its own exercise type [3][4].

3. Band U3 — Abstract Algebra (groups, rings, fields). Topics: group axioms, Lagrange’s theorem, cyclic groups, homomorphisms/isomorphisms, quotient groups, basic ring/field theory. Auto-grading: numeric/structural answers (order of an element, is this map a homomorphism — yes/no with a required counterexample element if no), Cayley-table completion, multiple-choice on “which axiom fails here.”

4. Band U4 — Real Analysis. Topics: sequences/limits, ε-δ continuity, differentiability, Riemann integration, series convergence tests. Auto-grading: numeric answer (find N such that |a_n - L| < ε), multiple-choice on which convergence test applies, and counterexample entry (“give a sequence that converges pointwise but not uniformly”) checked against a library of known-valid counterexamples plus a symbolic/numeric verifier (evaluate the candidate at sample points).

5. Band U5 — Linear Algebra beyond the intro course. Topics: eigenvalues/eigenvectors, diagonalization, Jordan form, inner product spaces, spectral theorem. Auto-grading: fully numeric/symbolic — this band is essentially free with a SymPy-equivalent CAS backend (the STACK/Maxima model applies almost directly) [17][18].

6. Band U6 — Combinatorics & Number Theory (olympiad-flavored). Topics: pigeonhole, invariants, modular arithmetic, generating functions, extremal combinatorics — modeled directly on Engel’s taxonomy and AoPS/WOOT structure [8][10]. Auto-grading: this band is the best fit for Math Challenge’s existing model — nearly all these problems have a single numeric or closed-form final answer, exactly like AMC/AIME/Putnam-style fill-in problems, so no new grading mechanism is needed beyond what the ladder already does lower down.

7. Band G1 — Topology. Topics: metric/topological spaces, compactness, connectedness, continuity, fundamental group basics. Auto-grading: multiple-choice (“is this space compact — yes/no, pick the covering that fails”), True/False with justification-selection (pick which of 4 candidate justifications is the valid one), since open-ended topological proofs are not mechanically checkable without formalization.

8. Band G2 — Measure Theory & Graduate Real Analysis. Topics: σ-algebras, Lebesgue measure, measurable functions, Lp spaces, dominated convergence. Auto-grading: mostly numeric (compute a Lebesgue integral, determine if a function is in L^p) plus multiple-choice on which convergence theorem applies to a given scenario — a near-direct mapping of Harvard’s real-analysis qualifying syllabus [13].

9. Band G3 — Complex Analysis. Topics: holomorphicity, Cauchy’s theorem, residues, conformal maps, Riemann mapping theorem. Auto-grading: numeric (evaluate a contour integral via residues — a classic CAS-checkable task) plus multiple-choice on singularity classification.

10. Band G4 — Algebraic Topology / Differential Geometry. Topics: homology/cohomology computation for standard spaces (spheres, tori, projective spaces), curvature of standard surfaces. Auto-grading: numeric (Betti numbers, Euler characteristic) — computable and checkable — but genuine proof content (e.g., “prove Poincaré duality for this space”) is not auto-gradable and should be presented as read-only “worked example” content, not as a scored challenge.

11. Band PhD-1 — PDEs & Probability (qualifying-exam core). Topics: heat/wave/Laplace equations, weak solutions, Sobolev embedding basics; measure-theoretic probability, characteristic functions, central limit theorem. Auto-grading: numeric solution-checking for canonical PDEs (verify a candidate solution satisfies the PDE and boundary conditions via direct substitution — purely mechanical and CAS-friendly) and probability computation questions.

12. Band PhD-Lean — “Formally Verified” capstone track, clearly labeled as different from the rest. Topics: a curated sequence of small lemmas (in the spirit of the Natural Number Game) building toward one nontrivial result, authored in Lean 4 against mathlib. Auto-grading: the compiler itself is the grader — a proof is graded pass/fail by successful compilation, with zero grading ambiguity, at the cost of a steep authoring investment (each exercise needs a Lean-checkable skeleton) and a real learning-curve cost for the player (Lean syntax, not just mathematics) [20][21].

13. Explicit non-goal: free-form natural-language proof grading by AI, as a scored (not tutor-feedback) mechanism. Given IMO-GradingBench’s ~52-54% blind-grading agreement with human judges even from frontier models in 2025-2026 [22], Math Challenge should not ship a feature that assigns a pass/fail or numeric score to student-written prose proofs via LLM judgment alone. It is appropriate, however, for the existing “AI tutor feedback after each challenge” to give qualitative, non-scoring commentary on a submitted proof sketch (this is a coaching feature, not a graded assessment, so a wrong or overconfident judgment is a UX quality issue, not a grading-integrity issue) — this distinction (feedback vs. score) is exactly what keeps the PhD-mode bands above honest about what “auto-gradable” means.

14. Cross-cutting mechanism: adopt RefGrader’s key idea — always grade against a reference, never blind — for any AI-assisted judgment used anywhere in PhD mode. Since reference-based agentic grading measurably outperforms blind grading [22][27], any place the tutor evaluates open-ended reasoning (not just the no-go case above) should always be given the canonical solution/rubric as context, never asked to judge a proof cold.

Open questions for the project owner

1. Should “PhD mode” include the Lean-checked capstone track (item 12) given its authoring cost, or stay entirely within numeric/multiple-choice/counterexample formats?
2. Is a coaching-only (non-scored) AI proof-sketch review acceptable for the top bands, or does the product need every challenge to produce a hard pass/fail score?
3. Should band boundaries follow MSC top-level codes strictly (for a “browse by MSC area” feature) or stay organized around the PhD-qualifying-exam core (which is narrower and more pedagogically standard)?
4. Is there appetite for licensing/integrating an existing CAS-backed engine (STACK’s Maxima pipeline is open-source and Moodle-native) rather than building numeric/symbolic equivalence checking from scratch?