Research-math reasoning, judged beyond raw solved counts.

Strengths: the best full-run result so far, with decisive obstruction finding, broad theorem deployment, 78 A-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 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.