← All benchmarks

ArXivLean 09/2026

Math

This MathArena track asks models to prove or disprove 53 conjectures formalized in Lean 4.34.1 from September 2026 arXiv papers; a submission states its verdict by proving either the conjecture or its negation, and a problem counts only if that Lean proof passes MathArena's checker. Earlier ArXivLean releases asked only for proofs, so this prove-or-disprove protocol is its own factor group. Scores average observed problem attempts; the item count records distinct problems, not a single-run binomial denominator.

Top models (higher is better)