Research & models Oct 22, 2026

Trend · preprint October 19

Maestro, mini-Lean split on harness value; samples are small

Two preprints point in different directions on whether gains in Lean theorem proving come from the harness or the base model: Maestro says swapping in its orchestration harness on the same base model solves 34 of 48 problems against 19 for native agents, while mini-Lean says a generic coding agent with a minimal harness is enough. Lean is a formal language for mathematical proofs. Maestro is a harness that coordinates several agents, and arXivLean is a set of Lean problems. Maestro self-reports solving 34 of the 48 problems in the June 2026 edition of arXivLean, against 19 for the native agents Claude Code or Codex; the paper doesn't list the authors' affiliations (arXiv 2610.25920, 2026-10-19). Maestro says both sides used the same base model. On October 12, mini-Lean, by Sanjeev Arora of Princeton and colleagues, wrote that "a generic coding agent with a minimal harness can already achieve strong performance on Lean benchmarks," self-reporting that on the 12 problems of Putnam 2025, Gemini 3.8 Flash solved 7 against 4 for the rival AxProverBase (arXiv 2610.17331, 2026-10-12). The two papers use different harness designs and problem sets, so one doesn't rebut the other on the same test. Both problem sets are small: with 12 and 48 problems, a few answers either way would change the conclusion. Our reading: current evidence can't yet say whether a harness is worth development resources. Only a retest with the same harness design and a larger problem set would separate gains from the harness and from the base model.