Research-math reasoning, judged beyond raw solved counts.

Strengths: the numerical leader, with 104 A-grade and 112 B-grade results, only 10 C-grade rows, no D/F/M rows, and 54 A-grade results that it conservatively labelled partial or triage. Its confidence is meaningfully calibrated, and the closed-book run produces unusually deep, self-contained research progress. Weaknesses: 14 of 64 explicit strong claims are downgraded to B or C, several conclusions depend on reconstructed meanings for underdefined statements, and the lack of tools limits literature and certificate-level reproducibility. Post-training: preserve its calibrated, conservative partial labels while improving strong-verdict precision and adding tool-backed checks for citations, definitions, computation, and specialist arguments.

Strengths: balanced top-tier research yield, with 104 A-grade rows, only 13 C rows, distinctive constructions on Problems 79 and 166, deep partial progress, and useful confidence calibration (mean 0.786) in a closed-book, tool-free run. Weaknesses: 20 of 77 strong claims are downgraded to B or C; solved-label precision trails Astra, several claims resolve reconstructed definitions, and technically ambitious proofs need specialist reproduction. It also misses decisive ideas on Problems 20, 85, and 91. Post-training: preserve its calibrated confidence and original construction ability while requiring exact statement alignment, explicit remaining-gap checks, and reproducible theorem or certificate verification before strong verdicts.

Strengths: third numerically in the near-tied leading cluster and the strongest theorem closer, with the highest A-grade yield at 106, exceptional theorem and counterexample output, broad mathematical technique, and 43 self-labelled partials that already contain sound A-grade progress. Weaknesses: its confidence scores are compressed near one and do not identify which rows need review; 18 C-grade rows form a wider weak tail than Fable, Opus 5.5, or GPT-5.6, while seven B-grade and one C-grade strong claims require specialist reproduction or an unconditional argument. Post-training: calibrate confidence against proof status, retain its conservative verdict labeling, and add specialist verification signals for long sieve, Fourier, set-theoretic, and representation-theoretic arguments.

Strengths: the fourth-highest full-run score and the cleanest low-quality tail, with decisive obstruction finding, broad theorem deployment, 78 A-grade rows, only 6 C-grade rows, and no rejected strong claims. Weaknesses: 142 rows remain useful partials, often stopping at one-sided bounds, corrected formulations, reductions, or finite variants; literal and conditional wins are valid but not all equally deep discoveries. Post-training: target the remaining exact asymptotics, uniform analytic number theory, and extremal-stability gaps with stronger theorem-dependency and proof-completion signals.

Strengths: the leading Meta-family run, with 79 A-grade rows, 125 useful B-grade rows, 38 of 44 strong claims accepted as A, and 41 A-grade results conservatively labelled partial or triage. It combines deep scoped subtheorems, broad mathematical technique, and calibrated confidence (means 0.827 on A, 0.611 on B, and 0.467 on C). Weaknesses: Problem 44 falsely strengthens a prime-pattern theorem; 21 C rows retain analytic, uniformity, interpretation, or globalization gaps. Its A-grade yield remains below the leading cluster, and five B-grade strong claims resolve ambiguous source conventions. Difficult original arguments lack executable certificates and richer run manifests. Post-training: preserve its partial-depth and careful theorem extraction while requiring exact literature scope, source-definition alignment, and explicit missing-lemma checks before strong verdicts. Add reproducible verification for technically ambitious closures and calibrate confidence against theorem-dependency risk.

Strengths: decisive invariants, exact asymptotics, original constructions, and broad technical range, with 80 A-grade rows, 47 of 61 strong claims accepted as A, and no D/F/M grades. Thirty-two schema-valid partials receive A, showing substantial theorem-level progress without aggressive solved labels. Weaknesses: 82 rows end in runner fallback; useful raw reasoning often remains unfinished, repetitive, or poorly consolidated. The 3.337 schema-valid subset mean falls to 3.036 across the full run. Confidence clusters high for valid reports and is forced to zero for fallbacks, making it weakly informative about correctness. Attribution, reconstructed definitions, and long original analytic arguments also increase review cost. Post-training: prioritize stable answer completion, schema checks, and a final pass that removes abandoned branches and emits one coherent proof. Require exact theorem attribution, source-definition alignment, and reproducible specialist checks while preserving its mathematical ambition.

Strengths: reliable solved and counterexample labels, with 36 of 43 strong claims accepted as A, 79 A-grade rows overall, no D/F/M rows, compact constructive obstructions, and self-contained proofs. Confidence is well calibrated: approximately 0.77 on A rows, 0.58 on B rows, and 0.42 on C rows. Weaknesses: partial depth and theorem closure trail the leading cluster; 29 of 183 partials receive C, and several decisive arguments are missed. Six B-grade strong claims and the C-grade claim on Problem 118 depend on reconstructed definitions or incomplete scope; Problem 182 imports an extremal lower bound unavailable in the claimed generality. Post-training: preserve its cautious verdicts and calibrated confidence while strengthening exact statement alignment, theorem-hypothesis checks, and proof completion, especially for uniform analytic-number-theory estimates and local-to-global arguments.

Strengths: a major improvement over MiniMax M3, with 72 A-grade and 135 B-grade rows, compact divisor, parity, CRT, coloring, and finite-group obstructions, and much cleaner theorem-aware partial work. Forty-eight of 69 strong claims receive A, and useful mathematics survives all five runner fallbacks. Weaknesses: 135 rows remain B-grade; definition-dependent readings and missing uniformity, stability, or all-parameter arguments limit closure. Problems 28, 83, and 210 import unsupported theorem scope, while the finite base-graph calculation in Problem 23 is false. The worst mistakes are overconfident despite reasonable A/B/C confidence separation. Post-training: preserve its efficient construction ability while requiring exact theorem statements and hypotheses, executable finite replay before counterexample verdicts, definition alignment, and a final coherent report. Calibrate confidence against failed verification signals and train proof completion beyond useful reductions.

Strengths: the top GLM-family full run, with full coverage, 58 A-grade rows, 151 useful B-grade rows, and especially strong divisor, coloring, CRT/coset, and geometric obstruction finding. Weaknesses: Problems 28 and 31 show its main failure mode: an elegant cycle or sumset argument is promoted before the theorem scope or key step is secure; two additional strong claims remain C-grade. Post-training: train a final adversarial proof pass that checks implication direction, theorem hypotheses, and the weakest globalizing step before a solved label is emitted.

Strengths: broad research yield, with 65 A-grade and 133 B-grade rows, full coverage, short arithmetic obstructions, modular constructions, exact colorings, and strong statement debugging. Set systems and algebraic combinatorics are especially productive, and confidence generally separates A/B/C work meaningfully. Weaknesses: 12 of 46 strong claims remain below A, including one D and one F; 25 rows have material gaps and three are D/F overall. Theorem-scope errors on Problems 28 and 218 and heuristic or moment overclaims on Problems 51, 80, and 93 undermine otherwise polished arguments. High confidence on the worst strong claims and limited certificate packaging increase review risk. Post-training: preserve its constructive instincts while requiring exact theorem hypotheses, explicit uniformity and integrability checks, and a final distinction between proved results, heuristics, and reconstructed definitions. Add reproducible checks before promoting technically original work to strong verdicts.

Strengths: a strong Meta-family full run, with 57 A-grade rows, 130 useful B-grade rows, no D/F/M rows, and 51 of 63 strong claims accepted as A. It is especially effective at decisive obstructions, scoped reductions, and compact counterexamples. Weaknesses: 39 C-grade rows remain materially gappy, and 12 strong labels are downgraded to B or C because a theorem-scope leap, unresolved uniformity input, or local construction prevents full closure. Post-training: emphasize proof-completion checks, global-vs-local scope, and calibrated stopping when a strong research direction is not yet a theorem.

Strengths: strong completed reports, decisive modular, coloring, divisor, and finite-group obstructions, and 150 useful B-grade rows. Its 44 A grades and cleaner C band are a substantial improvement over Qwen 3.7 Max. Three A results survive inside runner trajectories, and 32 of 47 strong claims receive A. Weaknesses: 148 fallbacks leave the auditor reconstructing proofs from repeated or abandoned reasoning. The 3.246 schema-valid subset mean falls to 2.795 over the full run. A false finite construction on Problem 42 and theorem-scope failures on Problems 48 and 83 show insufficient replay and literature checking. Reconstructed definitions and confidence tied to serialization further limit reliability. Post-training: prioritize stable schema-valid completion, one consolidated surviving proof, exact finite arithmetic checks, and precise theorem hypotheses. Align the verdict, summary, evidence, and remaining gaps before strong labels, and calibrate confidence against mathematical verification rather than output formatting.

Strengths: the strongest Kimi-family full run, with decisive obstruction finding, compact counterexamples, strong theorem selection, 40 A-grade rows, and 143 useful B-grade rows. Weaknesses: 43 rows retain material gaps, and Problems 9, 38, and 125 show the main failure mode: a sketched lemma, long case analysis, or conditional construction is promoted to a solved or counterexample label too early. Post-training: reinforce theorem-dependency checks, unconditional-vs-conditional labeling, and a final proof-debt review before allowing strong verdicts.

Strengths: a high-yield full-bench entrant with decisive obstruction finding, strong theorem selection, 48 A-grade rows, 126 useful B-grade rows, and 30 accepted strong claims with no D/F strong-claim failures. Weaknesses: the 47 C-grade and 4 D-grade rows cluster around unproved analytic-number-theory uniformity, long case analyses, conditional theorem transfers, and mis-scoped interpretations; one row required a raw-preserving fallback. Post-training: emphasize proof closure, hypothesis and uniformity checks, verdict calibration, and machine-checkable certificate evidence before promoting promising research directions to strong claims.

Strengths: previous full-run leader, excellent at decisive obstructions, exact formulas, and literal counterexamples. Weaknesses: many isolated strong claims are conditional, wording-dependent, or partial-mislabeled. Post-training: our audited rows can train stronger verdict calibration: require theorem dependencies, literal-vs-natural statement tags, and a final “what remains unproved?” check before a solved label is allowed.

Strengths: creative earlier Kimi-family run, strong on compact constructions and counterexamples. Weaknesses: solved labels sometimes hide proof gaps, false uniformity assumptions, or theorem-scope drift. Post-training: our accepted-vs-rejected Kimi pairs are ideal for DPO and process-reward training focused on quantifier discipline, uniformity checks, and “creative idea but not yet proof” downgrades.

Strengths: best reviewer profile, strong gap accounting, and many well-scoped partials. Weaknesses: underclaims short decisive obstructions and sometimes keeps a solved subproblem in “partial” mode. Post-training: our data can teach partial-to-theorem extraction: when a divisor bound, coloring invariant, or literal obstruction already closes the statement, promote it confidently while preserving caveats.

Strengths: strong entrant with many real A/B partials and good theorem-aware reductions. Weaknesses: theorem importation is uneven; some partials cite stronger-than-available results or make local-to-global jumps. Post-training: our full partial audit can train theorem-scope verification: state the exact theorem used, check hypotheses, and classify each row as strong partial, useful partial, heuristic, or invalid.

Strengths: persistent exploratory reasoning, explicit constructions, statement debugging, informative confidence separation, and 121 useful B-grade rows alongside 22 A-grade results. Its best work gives clean finite classifications and decisive obstructions. Weaknesses: only 13 of 31 strong claims receive A; three are contradicted and one likely wrong. Failed approaches often remain beside the surviving argument, leaving the summary, verdict, and proof inconsistent. A 72-row C band, seven D/F rows, four missing problems, weak reproducibility packaging, and long responses increase review cost. Post-training: require a final consistency pass that removes failed attempts, restates the surviving proof, checks exact theorem scope and simple counterexamples, and aligns the headline, verdict, and remaining gaps before a solved label. Preserve its construction ability while improving coverage and proof completion.

Strengths: useful full-coverage corroborator with many reasonable theorem-family suggestions. Weaknesses: fewer decisive accepted results and a tendency to phrase plausible programs as if they were complete proofs. Post-training: our judge labels can train missing-lemma detection: separate proved statement, conjectural extension, and required external lemma before producing a final answer.

Strengths: full coverage and a few good compact obstructions, literal counterexamples, and underclaimed A-level partials. Weaknesses: C-heavy partial profile and unreliable solved labels, with many D/F strong claims caused by wrong theorem scope, wrong recurrence, or wrong problem interpretation. Post-training: our data can train solved-label discipline: demote bad proofs, preserve useful subclaims, and reward explicit statement parsing before invoking a theorem.