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