Domains and reasoning levels
Each cell shows available public-dev views as Natural language / Lean / Graph JSON. On small screens, scroll the table horizontally for L3–L5. A gap is not a proof-completion percentage. Shared questions can occur in several domain indexes but count once globally.
| Domain | L1 | L2 | L3 | L4 | L5 |
|---|---|---|---|---|---|
| Log-Concave Sampling | 1 / 0 / 1 | 1 / 1 / 1 | 2 / 2 / 0 | 3 / 1 / 0 | gap |
| SampleWiki research problems | 1 / 0 / 0 | gap | 3 / 2 / 0 | 2 / 0 / 0 | gap |
| Optimisation | 1 / 0 / 3 | 1 / 2 / 2 | 4 / 1 / 0 | 2 / 1 / 0 | gap |
| Riemannian Optimisation | 1 / 0 / 0 | gap | 3 / 2 / 0 | gap | gap |
| Statistical Optimal Transport | 1 / 0 / 1 | 1 / 1 / 1 | 2 / 1 / 0 | 1 / 1 / 0 | gap |
| Discrete Sampling | 1 / 0 / 0 | 0 / 1 / 0 | 4 / 2 / 0 | 1 / 0 / 0 | gap |
| Markov Chain Monte Carlo | 1 / 0 / 0 | 0 / 1 / 0 | 5 / 2 / 0 | 1 / 0 / 0 | gap |
What the levels mean
- L1 · Concepts and conventions
Identify definitions, objects, units, quantifiers or a directly supplied graph relation.
- L2 · Local derivation
Execute one mathematical mechanism with explicit hypotheses, or combine a few supplied structural facts.
- L3 · Multi-step proof and diagnosis
Coordinate several estimates, separate cases, exhibit a counterexample or diagnose an invalid inference.
- L4 · Cross-module composition
Compose results with real assumption adapters, measurable/integrable inputs and error/constant tracking.
- L5 · Research-level audit and transfer
Audit a source-grounded research argument or transport a proof mechanism while exposing unresolved interfaces and failure boundaries. No unsolved conjecture may be scored against an invented gold proof.
Author-assigned, track-specific provisional labels; empirical calibration is pending. Token count, code length, import depth and graph distance are not difficulty scores.
Graph QA distinguishes source-scanned module imports from replayed constant occurrences in selected compiled proof bodies. Compiler snapshots also emit a fixed whitelist of direct constants in unexpanded elaborated statements: this is not binder-role classification, inferred hypotheses, definition expansion or a full type dependency closure. Each uses an explicitly eligible, source-hashed local slice. Neither edges nor profiles certify mathematical necessity, conceptual equivalence or full dependency closure; an absent induced path is not full-closure independence, and an absent direct constant is not absence after unfolding or proof derivation. Compiler replay, editorial admission and empirical calibration are separate. Richer source-proof and conceptual-hypergraph questions require their own reviewed evidence.
29 of 29 mathematical cores currently have AI editorial acceptance. Structural editorial status: complete-for-current-tasks. Empirical calibration remains open. L5 is a planned research-audit tier, not a claim of solved open problems.