Math RefereeHow we review
This notebook collects independent, AI-assisted examinations of mathematical manuscripts in the OpenAI mathematics collection. A review records particular arguments and evidence, the reviewers' coverage, and remaining questions.
Start with the argument
Each paper has a reading page containing the manuscript, its proposed argument, the claim index and a dependency map. Panel commentary has its own page and is loaded only when opened. You can record an independent assessment on the reading page; those notes stay in your browser and can be exported as text.
Read dependency edges precisely
Edges point from a prerequisite to its consumer. A literal reference is a candidate dependency. An annotated proof input is an attributed interpretation supported by a source passage. Background, explicitly excluded inputs and conditional inputs keep their own labels. These relations are not kernel proof certificates; a reference cycle alone does not establish mathematical circularity.
The long quasi-Riemann roadmap indexes 67 claims and 28 references. It contains 81 annotated relations, including 61 annotated proof inputs, alongside many literal source references and candidate relations. Those categories stay distinct.
Understand the assessments
A demonstrated error needs a precise invalid inference or verified counterexample. An unverified step records a remaining obligation. A completed model response establishes that a review returned, not that a theorem is true. Independent model agreement is supplementary evidence; source checking and formal certificates retain separate attribution. Transport failures and token exhaustion have no invented mathematical verdict.
The OpenAI primary is GPT-6.1 Sol; GPT-6 Astra at max is available for hard cases. The Anthropic primary is Opus 5.5 at max, with Fable 5.1 available for independent criticism or escalation. Each historical review records the models and effort actually used. Today's defaults are not substituted into earlier campaigns.
Formalization and execution
Static source inspection, a successful build, target axiom inspection and strict statement comparison are different checks. The quasi-Riemann source audit fetched 2,924 local imports and 19 relevant patched external modules. Lean 4.34.1 was installed on October 13, and a separate core-Lean smoke proof compiled. The target paper build, target axiom report and strict comparator have not yet been run.
Where a decision model could help
Our optional SubQ Snap pilot asks a typed decision model to classify source-backed dependency candidates as proof input, background, explicitly excluded, or insufficient context. The state would contain the claim, its supplied proof, the proposed prerequisite and the passage connecting them. Code would still resolve labels, check exact quotes and detect graph cycles.
Other useful narrow decisions include checking proof attachment, matching an objection to its quoted evidence, and selecting retrieval, exact computation, additional reasoning or human follow-up. These decisions guide work allocation; mathematical conclusions still require their supporting argument.
Start in shadow mode on independently labeled source passages, preserving the existing pipeline. Split calibration and evaluation by paper. Measure missed proof inputs, false promotions, abstention, erroneous cycle creation, latency and cost. A model's confidence describes its answer distribution and is not the probability that a mathematical theorem is true. Production routing and graph mutation remain disabled.
SubQ Snap pilot — October 13, 2026
The first bounded run returned 22 valid decisions: 12/12 agreement on simple curator-authored controls and 9/10 agreement with existing source-audit annotations on quasi-Riemann passages. These annotations are not independent human ground truth. One disagreement named the whole Dunn–Radziwiłł reference, which contains both an explicitly used cusp-expansion result and an explicitly excluded conditional prime asymptotic. When asked separately about those two results, SubQ matched both source roles. That follow-up is a post-hoc scoping check, not a held-out evaluation. The graph remains unchanged.
Across the 24 requests, reported input usage was 9,666 tokens, giving a usage-based estimate of $0.0004833 at the published $0.05 per million input tokens, with output free. This is API-contract and scoping evidence, not evidence of research-level mathematical accuracy. The next evaluation needs independently labeled result-level passages and a split by paper.
SubQ typed Decisions API, SubQ model pricing, decision confidence semantics.
Idea provenance
An antecedent in the mathematical literature, a method used in a finished proof, and a documented step in a model's discovery process are different evidence. References and textual similarity alone do not establish what a generating model read, retrieved or was supplied. Provenance notes retain explicit uncertainties.
Records
Every reading page identifies the reviewed repository commit and manuscript hashes. The local checkout is checked separately for changes to the selected files. A later commit does not make an unchanged manuscript a new paper. Downloads include an export manifest with hashes of the curated files. Original request logs, reasoning streams, credentials, private grading maps and curator keys are outside these site packages. The dated reports distinguish collected usage from estimated or unknown charges.