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 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: the best 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: 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: 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.