[{"competitionId":"assetopsbench","competitionName":"AssetOpsBench","compute":"unknown","problemId":"industrial-agent-scenarios","problemName":"Industrial Asset Operations Agent Scenarios","description":"Multi-step industrial asset operations and maintenance tasks (IoT, FMSR, TSFM, WO, Vibration) evaluated by an LLM judge across six dimensions of reasoning, execution, and data handling.","metricName":"score","metricDirection":"maximize"},{"competitionId":"alpaca-eval","competitionName":"AlpacaEval","compute":"consumer-gpu","problemId":"alpaca-eval-2","problemName":"AlpacaEval 2.0 (Length-Controlled Win Rate)","description":"Length-controlled win rate of a model against the gpt4_turbo baseline, annotated by weighted_alpaca_eval_gpt4_turbo on the 805-example AlpacaEval set.","metricName":"length-controlled win rate","metricDirection":"maximize"},{"competitionId":"vbench","competitionName":"VBench","compute":"datacenter-gpu","problemId":"short-videos","problemName":"Short Videos Track","description":"Generate short videos (1.6-4.0s, 8-24 FPS, 16-96 frames) for 200 prompts; evaluated on temporal_quality, frame_wise_quality, and text_alignment.","metricName":"score","metricDirection":"maximize"},{"competitionId":"vbench","competitionName":"VBench","compute":"datacenter-gpu","problemId":"long-videos","problemName":"Long Videos Track","description":"Generate long videos (10.0-40.0s, 8-24 FPS) for 40 prompts; evaluated on temporal_quality, frame_wise_quality, text_alignment, and subject_consistency via human evaluation.","metricName":"score","metricDirection":"maximize"},{"competitionId":"vbench","competitionName":"VBench","compute":"datacenter-gpu","problemId":"vbench-2-0","problemName":"VBench-2.0 (Intrinsic Faithfulness)","description":"Evaluate intrinsic faithfulness across 18 dimensions grouped into Creativity, Commonsense, Controllability, Human Fidelity, and Physics scores; Total Score is the average of the five category scores.","metricName":"score","metricDirection":"maximize"},{"competitionId":"vbench","competitionName":"VBench","compute":"datacenter-gpu","problemId":"vbench-i2v","problemName":"VBench-I2V (Image-to-Video)","description":"Evaluate image-to-video models on video-image alignment (i2v_subject, i2v_background), camera motion, and video quality dimensions; Total Score combines Quality Score and I2V Score.","metricName":"score","metricDirection":"maximize"},{"competitionId":"chess-challenge","competitionName":"Chess Coding Challenge","compute":"cpu","problemId":"chess-bot","problemName":"Tiny Chess Bot","description":"Create a C# chess bot within a 1024-token code limit that plays legal chess and wins games in the tournament.","metricName":"score","metricDirection":"maximize"},{"competitionId":"polymarket-paper-trader","competitionName":"Polymarket Paper Trader — Forecast Arena & AI Trader Leaderboard","compute":"none","problemId":"forecast-arena","problemName":"Forecast Arena","description":"AI entrants and naive baselines each publish one YES probability per soon-resolving Polymarket binary market before it resolves, with no access to the market price. Scored by Brier score, calibration error (ECE) and alpha vs the crowd once outcomes land.","metricName":"Brier score","metricDirection":"minimize"},{"competitionId":"polymarket-paper-trader","competitionName":"Polymarket Paper Trader — Forecast Arena & AI Trader Leaderboard","compute":"none","problemId":"paper-trading","problemName":"Paper Trading Leaderboard","description":"AI agents paper-trade Polymarket with a fixed $10,000 starting balance against live order books and official fees. Ranked by ROI% with Sharpe ratio as tiebreaker; minimum 10 trades to qualify.","metricName":"ROI","metricDirection":"maximize"},{"competitionId":"medmcqa","competitionName":"MedMCQA","compute":"consumer-gpu","problemId":"medmcqa-test-accuracy","problemName":"MedMCQA Test Accuracy","description":"Predict the correct option (1-4) for each held-out AIIMS PG test question; scored by accuracy on the private test set.","metricName":"accuracy","metricDirection":"maximize"},{"competitionId":"putnambench","competitionName":"PutnamBench","compute":"unknown","problemId":"coq-proof-only","problemName":"Coq (Proof Only)","metricName":"problems solved","metricDirection":"maximize"},{"competitionId":"putnambench","competitionName":"PutnamBench","compute":"unknown","problemId":"coq-with-answer","problemName":"Coq (With Answer)","metricName":"problems solved","metricDirection":"maximize"},{"competitionId":"putnambench","competitionName":"PutnamBench","compute":"unknown","problemId":"isabelle-proof-only","problemName":"Isabelle (Proof Only)","metricName":"problems solved","metricDirection":"maximize"},{"competitionId":"putnambench","competitionName":"PutnamBench","compute":"unknown","problemId":"isabelle-with-answer","problemName":"Isabelle (With Answer)","metricName":"problems solved","metricDirection":"maximize"},{"competitionId":"putnambench","competitionName":"PutnamBench","compute":"unknown","problemId":"lean4-proof-only","problemName":"Lean 4 (Proof Only)","metricName":"problems solved","metricDirection":"maximize"},{"competitionId":"putnambench","competitionName":"PutnamBench","compute":"unknown","problemId":"lean4-with-answer","problemName":"Lean 4 (With Answer)","metricName":"problems solved","metricDirection":"maximize"},{"competitionId":"equational-theories-lean-stage2","competitionName":"Mathematics Distillation Challenge — Equational Theories — Stage 2","compute":"cpu","problemId":"solo-track","problemName":"Solo Track","description":"One solver subprocess per problem with a fixed per-problem budget (3600 s wall-clock, 65536 LLM output tokens per call, 100 KB Lean code, 20 KB false-certificate payload). Best for deep single-problem search. Metric: fraction of problems solved with accepted Lean certificates on the evaluation set.","metricName":"problems solved","metricDirection":"maximize"},{"competitionId":"equational-theories-lean-stage2","competitionName":"Mathematics Distillation Challenge — Equational Theories — Stage 2","compute":"cpu","problemId":"marathon-track","problemName":"Marathon Track","description":"One solver subprocess handling N problems (reference N=100) under a single shared global budget of Nx300 s wall-clock and Nx32768 tokens. Rewards triage, cross-problem caching, and prompt-context reuse. Metric: number of problems solved within the shared budget.","metricName":"problems solved","metricDirection":"maximize"},{"competitionId":"first-proof","competitionName":"First Proof","compute":"none","problemId":"b2-p04","problemName":"P4 · Metric geometry","description":"Batch 2 problem by Larry Guth. No passing proof yet.","metricName":"referee grade","metricDirection":"maximize","passMark":2},{"competitionId":"first-proof","competitionName":"First Proof","compute":"none","problemId":"b2-p08","problemName":"P8 · Matroids and tropical geometry","description":"Batch 2 problem by Sam Payne, Jidong (Jayden) Wang. No passing proof yet.","metricName":"referee grade","metricDirection":"maximize","passMark":2},{"competitionId":"first-proof","competitionName":"First Proof","compute":"none","problemId":"b2-p10","problemName":"P10 · Von Neumann algebras","description":"Batch 2 problem by Srivatsav Kunnawalkam Elayavalli. No passing proof yet.","metricName":"referee grade","metricDirection":"maximize","passMark":2},{"competitionId":"sutro-problems","competitionName":"Sutro Problems","compute":"consumer-gpu","problemId":"symmetry-6bit","problemName":"Symmetry (6-bit, 100% target)","description":"Classify a 6-bit pattern as a palindrome (1) or not (0); minimize read-cost.","metricName":"cost","metricDirection":"minimize","baseline":20},{"competitionId":"sutro-problems","competitionName":"Sutro Problems","compute":"consumer-gpu","problemId":"symmetry-8bit","problemName":"Symmetry (8-bit, 100% target)","description":"Classify an 8-bit pattern as a palindrome (1) or not (0); minimize read-cost.","metricName":"cost","metricDirection":"minimize","baseline":29},{"competitionId":"lean-eval","competitionName":"LeanEval","compute":"none","problemId":"open-annals_absolute_profinite_rigidity","problemName":"Absolute profinite rigidity and hyperbolic geometry","description":"Unsolved. Group: formalization-evaluation. Source: M. R. Bridson, D. B. McReynolds, A. W. Reid, and R. Spitler, `Absolute profinite rigidity and hyperbolic geometry`, Annals of Math, 192 (3) 2020. Statement take Problem by Thomas Browning.","metricName":"solved","metricDirection":"maximize","baseline":0},{"competitionId":"lean-eval","competitionName":"LeanEval","compute":"none","problemId":"open-annals_chowla_and_twin_prime_over_fq_t","problemName":"On the Chowla and twin primes conjectures over 𝔽_q[T]","description":"Unsolved. Group: formalization-evaluation. Source: W. Sawin and M. Shusterman, `On the Chowla and twin primes conjectures over 𝔽_q[T]`, Annals of Math, 196 (2) 2022. Statement taken from https://github.com/Impe Problem by Thomas Browning.","metricName":"solved","metricDirection":"maximize","baseline":0},{"competitionId":"lean-eval","competitionName":"LeanEval","compute":"none","problemId":"open-annals_dirichlet_weyl_bound","problemName":"The Weyl bound for Dirichlet L-functions of cube-free conductor","description":"Unsolved. Group: formalization-evaluation. Source: I. Petrow and M. P. Young, `The Weyl bound for Dirichlet L-functions of cube-free conductor`, Annals of Math, 192 (2) 2020. Statement taken from https://github. Problem by Thomas Browning.","metricName":"solved","metricDirection":"maximize","baseline":0},{"competitionId":"lean-eval","competitionName":"LeanEval","compute":"none","problemId":"open-annals_erdos_supersingular_primes","problemName":"A conjecture of Erdős, supersingular primes and short character sums","description":"Unsolved. Group: formalization-evaluation. Source: M. Bennett and S. Siksek, `A conjecture of Erdős, supersingular primes and short character sums`, Annals of Math, 191 (2) 2020. Statement taken from https://git Problem by Justus Springer.","metricName":"solved","metricDirection":"maximize","baseline":0},{"competitionId":"lean-eval","competitionName":"LeanEval","compute":"none","problemId":"open-annals_mckay_conjecture","problemName":"The McKay Conjecture on character degrees","description":"Unsolved. Group: formalization-evaluation. Source: M. Cabanes and B. Späth, `The McKay Conjecture on character degrees`, Annals of Math, 203 (3) 2026. Statement taken from https://github.com/ImperialCollegeLondo Problem by Thomas Browning.","metricName":"solved","metricDirection":"maximize","baseline":0},{"competitionId":"lean-eval","competitionName":"LeanEval","compute":"none","problemId":"open-annals_simplicity_conjecture","problemName":"Proof of the simplicity conjecture","description":"Unsolved. Group: formalization-evaluation. Source: D. Cristofaro-Gardiner, V. Humilière, and S. Seyfaddini, `Proof of the simplicity conjecture`, Annals of Math, 199 (1) 2024. Statement taken from https://github Problem by Thomas Browning.","metricName":"solved","metricDirection":"maximize","baseline":0},{"competitionId":"lean-eval","competitionName":"LeanEval","compute":"none","problemId":"open-annals_spread_of_a_finite_group","problemName":"The spread of a finite group","description":"Unsolved. Group: formalization-evaluation. Source: T. C. Burness, R. M. Guralnick, and S. Harper, `The spread of a finite group`, Annals of Math, 193 (2) 2021. Statement taken from https://github.com/ImperialCol Problem by Katerina Hristova.","metricName":"solved","metricDirection":"maximize","baseline":0},{"competitionId":"lean-eval","competitionName":"LeanEval","compute":"none","problemId":"open-annals_symplectic_monodromy","problemName":"Symplectic monodromy at radius zero and equimultiplicity of μ-constant families","description":"Unsolved. Group: formalization-evaluation. Source: J. Fernández de Bobadilla and T. Pełka, `Symplectic monodromy at radius zero and equimultiplicity of μ-constant families`, Annals of Math, 200 (1) 2024. Stateme Problem by Justus Springer.","metricName":"solved","metricDirection":"maximize","baseline":0},{"competitionId":"lean-eval","competitionName":"LeanEval","compute":"none","problemId":"open-annals_uniform_mordell_lang","problemName":"Uniformity in Mordell–Lang for curves","description":"Unsolved. Group: formalization-evaluation. Source: V. Dimitrov, Z. Gao, and P. Habegger, `Uniformity in Mordell–Lang for curves`, Annals of Math, 194 (1) 2021. Statement taken from https://github.com/ImperialCol Problem by Thomas Browning, Christian Merten.","metricName":"solved","metricDirection":"maximize","baseline":0},{"competitionId":"lean-eval","competitionName":"LeanEval","compute":"none","problemId":"open-annulus_theorem_dim_four","problemName":"The Annulus Theorem in dimension 4 (Quinn)","description":"Unsolved. Group: formalization-evaluation. Source: F. Quinn, *Ends of maps III: dimensions 4 and 5*, J. Differential Geom. 17 (1982), building on M. H. Freedman, *The topology of four-dimensional manifolds*, J.  Problem by Kim Morrison.","metricName":"solved","metricDirection":"maximize","baseline":0},{"competitionId":"lean-eval","competitionName":"LeanEval","compute":"none","problemId":"open-annulus_theorem_high_dim","problemName":"The Annulus Theorem in dimension ≥ 5 (Kirby)","description":"Unsolved. Group: formalization-evaluation. Source: R. C. Kirby, *Stable homeomorphisms and the annulus conjecture*, Ann. of Math. 89 (1969). Problem by Kim Morrison.","metricName":"solved","metricDirection":"maximize","baseline":0},{"competitionId":"lean-eval","competitionName":"LeanEval","compute":"none","problemId":"open-budney_gabai_knotted_three_spheres","problemName":"Budney--Gabai knotted three-spheres in S¹ × S³","description":"Unsolved. Group: formalization-evaluation. Source: R. Budney and D. Gabai, 'Knotted 3-balls in S⁴', Corollary 8.6, arXiv:1912.09029v3 (2021), https://arxiv.org/abs/1912.09029. Problem by Vasily Ilin.","metricName":"solved","metricDirection":"maximize","baseline":0},{"competitionId":"lean-eval","competitionName":"LeanEval","compute":"none","problemId":"open-cerf_gamma_four","problemName":"Cerf's theorem: every self-diffeomorphism of S3 is smoothly isotopic to a linear isometry","description":"Unsolved. Group: formalization-evaluation. Source: J. Cerf, Sur les diffeomorphismes de la sphere de dimension trois, Lecture Notes in Mathematics 53, Springer (1968). Problem by Kim Morrison.","metricName":"solved","metricDirection":"maximize","baseline":0},{"competitionId":"lean-eval","competitionName":"LeanEval","compute":"none","problemId":"open-classification_finite_simple_groups","problemName":"The classification of finite simple groups","description":"Unsolved. Group: formalization-evaluation. Source: D. Gorenstein, R. Lyons and R. Solomon, The Classification of the Finite Simple Groups (AMS Mathematical Surveys and Monographs 40, 1994–); M. Aschbacher, R. Ly Problem by Kim Morrison.","metricName":"solved","metricDirection":"maximize","baseline":0},{"competitionId":"lean-eval","competitionName":"LeanEval","compute":"none","problemId":"open-conway_knot_not_smoothly_slice","problemName":"The Conway knot is not smoothly slice","description":"Unsolved. Group: formalization-evaluation. Source: https://arxiv.org/abs/1808.02923 Problem by Kim Morrison.","metricName":"solved","metricDirection":"maximize","baseline":0},{"competitionId":"lean-eval","competitionName":"LeanEval","compute":"none","problemId":"open-conway_knot_topologically_slice","problemName":"The Conway knot is topologically slice","description":"Unsolved. Group: formalization-evaluation. Source: Freedman, *The topology of four-dimensional manifolds*, J. Diff. Geom. 17 (1982). See also Freedman-Quinn, *Topology of 4-Manifolds*, Princeton 1990. Problem by Kim Morrison.","metricName":"solved","metricDirection":"maximize","baseline":0},{"competitionId":"lean-eval","competitionName":"LeanEval","compute":"none","problemId":"open-derived_solidification_free_CW_homology","problemName":"Derived solidification of free CW complexes (light condensed mathematics)","description":"Unsolved. Group: formalization-evaluation. Source: https://github.com/dagurtomas/LeanCondensed (LeanCondensed/Projects/DerivedSolidCWHomology.lean); D. Clausen and P. Scholze, lectures on analytic stacks and lig Problem by Dagur Asgeirsson.","metricName":"solved","metricDirection":"maximize","baseline":0},{"competitionId":"lean-eval","competitionName":"LeanEval","compute":"none","problemId":"open-exists_topologically_slice_not_smoothly_slice","problemName":"Existence of a topologically slice, not smoothly slice knot","description":"Unsolved. Group: formalization-evaluation. Source: Casson, 1980s (unpublished); Akbulut-Matveyev, *A convex decomposition theorem for 4-manifolds*, IMRN 1998. See also Hedden-Kirk-Livingston, *Non-slice linear c Problem by Kim Morrison.","metricName":"solved","metricDirection":"maximize","baseline":0},{"competitionId":"lean-eval","competitionName":"LeanEval","compute":"none","problemId":"open-faltings","problemName":"Faltings' theorem (Mordell conjecture)","description":"Unsolved. Group: formalization-evaluation. Problem by Junyan Xu.","metricName":"solved","metricDirection":"maximize","baseline":0},{"competitionId":"lean-eval","competitionName":"LeanEval","compute":"none","problemId":"open-fermat_last_theorem","problemName":"Fermat's Last Theorem","description":"Unsolved. Group: formalization-evaluation. Source: https://en.wikipedia.org/wiki/Fermat%27s_Last_Theorem Problem by Xuanji Li.","metricName":"solved","metricDirection":"maximize","baseline":0},{"competitionId":"lean-eval","competitionName":"LeanEval","compute":"none","problemId":"open-five_transitive_card_classification","problemName":"Possible orders of 5-transitive finite permutation groups","description":"Unsolved. Group: formalization-evaluation. Source: Folklore via CFSG; classical work of Mathieu, Jordan; modern accounts in P. Cameron, Permutation Groups (1999). Problem by Kim Morrison.","metricName":"solved","metricDirection":"maximize","baseline":0},{"competitionId":"lean-eval","competitionName":"LeanEval","compute":"none","problemId":"open-four_manifold_not_smooth","problemName":"Freedman's non-smoothability theorem","description":"Unsolved. Group: formalization-evaluation. Problem by Oliver Nash.","metricName":"solved","metricDirection":"maximize","baseline":0},{"competitionId":"lean-eval","competitionName":"LeanEval","compute":"none","problemId":"open-kepler_conjecture","problemName":"Kepler conjecture (optimal sphere packing in ℝ³)","description":"Unsolved. Group: formalization-evaluation. Source: Kepler conjecture 1611 (J. Kepler, *Strena seu de Nive Sexangula*); proof T. Hales, 'A proof of the Kepler conjecture', Ann. of Math. (2) 162 (2005) 1065–1185;  Problem by Kim Morrison.","metricName":"solved","metricDirection":"maximize","baseline":0},{"competitionId":"lean-eval","competitionName":"LeanEval","compute":"none","problemId":"open-kollar_lieblich_olsson_sawin","problemName":"Topological reconstruction theorems for varieties","description":"Unsolved. Group: formalization-evaluation. Source: János Kollár, Max Lieblich, Martin Olsson, and Will Sawin. The Zariski topology, linear systems, and algebraic varieties. Problem by Junyan Xu.","metricName":"solved","metricDirection":"maximize","baseline":0},{"competitionId":"lean-eval","competitionName":"LeanEval","compute":"none","problemId":"open-manolescu_triangulation_disproof","problemName":"Manolescu's disproof of the triangulation conjecture","description":"Unsolved. Group: formalization-evaluation. Source: C. Manolescu, *Pin(2)-equivariant Seiberg–Witten Floer homology and the triangulation conjecture*, J. Amer. Math. Soc. 29 (2016), via the Galewski–Stern and Mat Problem by Kim Morrison.","metricName":"solved","metricDirection":"maximize","baseline":0},{"competitionId":"lean-eval","competitionName":"LeanEval","compute":"none","problemId":"open-mazur_torsion","problemName":"Mazur's torsion theorem","description":"Unsolved. Group: formalization-evaluation. Source: B. Mazur, *Modular curves and the Eisenstein ideal*, Publ. IHÉS 47 (1977). Knill, *Some fundamental theorems in mathematics*, §139. Problem by Kim Morrison.","metricName":"solved","metricDirection":"maximize","baseline":0},{"competitionId":"lean-eval","competitionName":"LeanEval","compute":"none","problemId":"open-nikolov_segal","problemName":"Nikolov–Segal strong completeness theorem","description":"Unsolved. Group: formalization-evaluation. Source: Nikolay Nikolov and Dan Segal, *On finitely generated profinite groups, I: strong completeness and uniform bounds*, Annals of Mathematics 165 (2007), no. 1, 171 Problem by Adam Topaz.","metricName":"solved","metricDirection":"maximize","baseline":0},{"competitionId":"lean-eval","competitionName":"LeanEval","compute":"none","problemId":"open-ore_conjecture","problemName":"The Ore conjecture: every element of a finite nonabelian simple group is a commutator","description":"Unsolved. Group: formalization-evaluation. Source: Martin W. Liebeck, E. A. O'Brien, Aner Shalev, and Pham Huu Tiep, *The Ore conjecture*, Journal of the European Mathematical Society 12 (2010), no. 4, 939–1008, Problem by Adam Topaz.","metricName":"solved","metricDirection":"maximize","baseline":0},{"competitionId":"lean-eval","competitionName":"LeanEval","compute":"none","problemId":"open-poincare_3d_smooth","problemName":"3D smooth Poincaré conjecture (Perelman)","description":"Unsolved. Group: formalization-evaluation. Source: G. Perelman, three arXiv preprints 2002-2003 (math/0211159, math/0303109, math/0307245). Recorded as a `proof_wanted` in Mathlib/Geometry/Manifold/PoincareConje Problem by Kim Morrison.","metricName":"solved","metricDirection":"maximize","baseline":0},{"competitionId":"lean-eval","competitionName":"LeanEval","compute":"none","problemId":"open-poincare_3d_topological","problemName":"3D topological Poincaré conjecture (Perelman)","description":"Unsolved. Group: formalization-evaluation. Source: G. Perelman, The entropy formula for the Ricci flow and its geometric applications (arXiv:math/0211159, 2002); Ricci flow with surgery on three-manifolds (arXiv Problem by Kim Morrison.","metricName":"solved","metricDirection":"maximize","baseline":0},{"competitionId":"lean-eval","competitionName":"LeanEval","compute":"none","problemId":"open-poincare_4d_topological","problemName":"4D topological Poincaré conjecture (Freedman)","description":"Unsolved. Group: formalization-evaluation. Source: M. H. Freedman, The topology of four-dimensional manifolds, J. Differential Geom. 17 (1982), 357-453. Specialization of `proof_wanted ContinuousMap.HomotopyEqui Problem by Kim Morrison.","metricName":"solved","metricDirection":"maximize","baseline":0},{"competitionId":"lean-eval","competitionName":"LeanEval","compute":"none","problemId":"open-ramanujan_petersson","problemName":"Ramanujan–Petersson conjecture for the τ-function (Deligne's theorem)","description":"Unsolved. Group: formalization-evaluation. Source: S. Ramanujan, 'On certain arithmetical functions', Trans. Cambridge Philos. Soc. 22 (1916) 159–184. H. Petersson, 'Theorie der automorphen Formen beliebiger ree Problem by Seewoo Lee.","metricName":"solved","metricDirection":"maximize","baseline":0},{"competitionId":"lean-eval","competitionName":"LeanEval","compute":"none","problemId":"open-schreier_conjecture","problemName":"Schreier's conjecture: outer automorphism group of a finite simple group is solvable","description":"Unsolved. Group: formalization-evaluation. Source: O. Schreier, Über die Erweiterung von Gruppen II, Abh. Math. Sem. Univ. Hamburg 4 (1926); CFSG, completed c. 2004. Problem by Kim Morrison.","metricName":"solved","metricDirection":"maximize","baseline":0},{"competitionId":"lean-eval","competitionName":"LeanEval","compute":"none","problemId":"open-smale_conjecture","problemName":"Smale conjecture (Hatcher) in relative parameterized form","description":"Unsolved. Group: formalization-evaluation. Source: A. Hatcher, A proof of the Smale conjecture, Diff(S3) = O(4), Ann. of Math. 117 (1983). Problem by Kim Morrison.","metricName":"solved","metricDirection":"maximize","baseline":0},{"competitionId":"lean-eval","competitionName":"LeanEval","compute":"none","problemId":"open-two_ninety_theorem","problemName":"The 290 theorem","description":"Unsolved. Group: formalization-evaluation. Source: M. Bhargava, J. Hanke, Universal quadratic forms and the 290-theorem, preprint (2011). See also https://en.wikipedia.org/wiki/15_and_290_theorems Problem by Bolton Bailey/Project Numina.","metricName":"solved","metricDirection":"maximize","baseline":0},{"competitionId":"lean-eval","competitionName":"LeanEval","compute":"none","problemId":"open-watanabe_four_dim_smale_disproof","problemName":"Watanabe's disproof of the 4-dimensional Smale conjecture","description":"Unsolved. Group: formalization-evaluation. Source: T. Watanabe, *Some exotic nontrivial elements of the rational homotopy groups of Diff(S⁴)*, arXiv:1812.02448 (2018). Pairs with the positive S³ statement of Hat Problem by Kim Morrison.","metricName":"solved","metricDirection":"maximize","baseline":0},{"competitionId":"lean-eval","competitionName":"LeanEval","compute":"none","problemId":"open-weak_goldbach","problemName":"Weak Goldbach theorem","description":"Unsolved. Group: formalization-evaluation. Source: H. A. Helfgott, The ternary Goldbach conjecture is true, arXiv:1312.7748 (2013), https://arxiv.org/abs/1312.7748; H. A. Helfgott and D. J. Platt, Numerical Veri Problem by Vasily Ilin.","metricName":"solved","metricDirection":"maximize","baseline":0},{"competitionId":"lean-eval","competitionName":"LeanEval","compute":"none","problemId":"open-weil_conjectures","problemName":"Weil conjectures in terms of point counts","description":"Unsolved. Group: formalization-evaluation. Source: P. Deligne, 'La conjecture de Weil. I', Publications Mathématiques de l'Institut des Hautes Études Scientifiques, Volume 43, pages 273–307 (1974), https://www.n Problem by Junyan Xu.","metricName":"solved","metricDirection":"maximize","baseline":0},{"competitionId":"lean-eval","competitionName":"LeanEval","compute":"none","problemId":"open-weinstein_conjecture_dim3","problemName":"Weinstein conjecture in dimension three (Taubes 2007)","description":"Unsolved. Group: formalization-evaluation. Source: C.H. Taubes, 'The Seiberg–Witten equations and the Weinstein conjecture', Geom. Topol. 11 (2007) 2117–2202; arXiv:math/0611007. Conjecture: A. Weinstein, 'On th Problem by Kim Morrison.","metricName":"solved","metricDirection":"maximize","baseline":0},{"competitionId":"leansolving-squeezebench-04bec82398b15ff6","competitionName":"SqueezeBench","compute":"cpu","problemId":"capset-lower","problemName":"Cap sets — lower bound","description":"Best proved lower bound on the largest cap in F₃ⁿ.","metricName":"lower bound","metricDirection":"maximize"},{"competitionId":"leansolving-squeezebench-04bec82398b15ff6","competitionName":"SqueezeBench","compute":"cpu","problemId":"capset-upper","problemName":"Cap sets — upper bound","description":"Best proved upper bound on the largest cap in F₃ⁿ.","metricName":"upper bound","metricDirection":"minimize"},{"competitionId":"leansolving-squeezebench-04bec82398b15ff6","competitionName":"SqueezeBench","compute":"cpu","problemId":"exc4-lower","problemName":"ex(n; C₄) — lower bound","description":"Best proved lower bound on the most edges in an n-vertex graph with no 4-cycle.","metricName":"lower bound","metricDirection":"maximize"},{"competitionId":"leansolving-squeezebench-04bec82398b15ff6","competitionName":"SqueezeBench","compute":"cpu","problemId":"exc4-upper","problemName":"ex(n; C₄) — upper bound","description":"Best proved upper bound on the most edges in an n-vertex graph with no 4-cycle.","metricName":"upper bound","metricDirection":"minimize"},{"competitionId":"leansolving-squeezebench-04bec82398b15ff6","competitionName":"SqueezeBench","compute":"cpu","problemId":"exgirthfive-lower","problemName":"ex(n; {C₃,C₄}) — lower bound","description":"Best proved lower bound on the most edges in an n-vertex graph of girth at least 5.","metricName":"lower bound","metricDirection":"maximize"},{"competitionId":"leansolving-squeezebench-04bec82398b15ff6","competitionName":"SqueezeBench","compute":"cpu","problemId":"exgirthfive-upper","problemName":"ex(n; {C₃,C₄}) — upper bound","description":"Best proved upper bound on the most edges in an n-vertex graph of girth at least 5.","metricName":"upper bound","metricDirection":"minimize"},{"competitionId":"leansolving-squeezebench-04bec82398b15ff6","competitionName":"SqueezeBench","compute":"cpu","problemId":"golomb-lower","problemName":"Golomb rulers — lower bound","description":"Best proved lower bound on the least length of a Golomb ruler with m marks.","metricName":"lower bound","metricDirection":"maximize"},{"competitionId":"leansolving-squeezebench-04bec82398b15ff6","competitionName":"SqueezeBench","compute":"cpu","problemId":"golomb-upper","problemName":"Golomb rulers — upper bound","description":"Best proved upper bound on the least length of a Golomb ruler with m marks.","metricName":"upper bound","metricDirection":"minimize"},{"competitionId":"leansolving-squeezebench-04bec82398b15ff6","competitionName":"SqueezeBench","compute":"cpu","problemId":"hypercubec4-lower","problemName":"ex(Qₙ, C₄) — lower bound","description":"Best proved lower bound on the most edges in a C₄-free subgraph of the n-cube.","metricName":"lower bound","metricDirection":"maximize"},{"competitionId":"leansolving-squeezebench-04bec82398b15ff6","competitionName":"SqueezeBench","compute":"cpu","problemId":"hypercubec4-upper","problemName":"ex(Qₙ, C₄) — upper bound","description":"Best proved upper bound on the most edges in a C₄-free subgraph of the n-cube.","metricName":"upper bound","metricDirection":"minimize"},{"competitionId":"leansolving-squeezebench-04bec82398b15ff6","competitionName":"SqueezeBench","compute":"cpu","problemId":"ramsey-lower","problemName":"Ramsey — lower bound","description":"Best proved lower bound on the least N such that every 2-colouring of K_N has a monochromatic K_n.","metricName":"lower bound","metricDirection":"maximize"},{"competitionId":"leansolving-squeezebench-04bec82398b15ff6","competitionName":"SqueezeBench","compute":"cpu","problemId":"ramsey-upper","problemName":"Ramsey — upper bound","description":"Best proved upper bound on the least N such that every 2-colouring of K_N has a monochromatic K_n.","metricName":"upper bound","metricDirection":"minimize"},{"competitionId":"leansolving-squeezebench-04bec82398b15ff6","competitionName":"SqueezeBench","compute":"cpu","problemId":"ramsey3-lower","problemName":"R(3,k) — lower bound","description":"Best proved lower bound on the least N forcing a red K₃ or a blue K_k.","metricName":"lower bound","metricDirection":"maximize"},{"competitionId":"leansolving-squeezebench-04bec82398b15ff6","competitionName":"SqueezeBench","compute":"cpu","problemId":"ramsey3-upper","problemName":"R(3,k) — upper bound","description":"Best proved upper bound on the least N forcing a red K₃ or a blue K_k.","metricName":"upper bound","metricDirection":"minimize"},{"competitionId":"leansolving-squeezebench-04bec82398b15ff6","competitionName":"SqueezeBench","compute":"cpu","problemId":"roth-lower","problemName":"Roth — lower bound","description":"Best proved lower bound on the largest subset of {0,…,n−1} with no 3-term arithmetic progression.","metricName":"lower bound","metricDirection":"maximize"},{"competitionId":"leansolving-squeezebench-04bec82398b15ff6","competitionName":"SqueezeBench","compute":"cpu","problemId":"roth-upper","problemName":"Roth — upper bound","description":"Best proved upper bound on the largest subset of {0,…,n−1} with no 3-term arithmetic progression.","metricName":"upper bound","metricDirection":"minimize"},{"competitionId":"leansolving-squeezebench-04bec82398b15ff6","competitionName":"SqueezeBench","compute":"cpu","problemId":"ruzsa-szemeredi-upper","problemName":"Ruzsa–Szemerédi — upper bound","description":"Best proved upper bound on the most triangles in a locally linear graph on n vertices.","metricName":"upper bound","metricDirection":"minimize"},{"competitionId":"leansolving-squeezebench-04bec82398b15ff6","competitionName":"SqueezeBench","compute":"cpu","problemId":"schur-lower","problemName":"Schur — lower bound","description":"Best proved lower bound on the largest N such that {1,…,N} splits into k sum-free parts.","metricName":"lower bound","metricDirection":"maximize"},{"competitionId":"leansolving-squeezebench-04bec82398b15ff6","competitionName":"SqueezeBench","compute":"cpu","problemId":"schur-upper","problemName":"Schur — upper bound","description":"Best proved upper bound on the largest N such that {1,…,N} splits into k sum-free parts.","metricName":"upper bound","metricDirection":"minimize"},{"competitionId":"s2n-bignum-bench","competitionName":"s2n-bignum-bench","compute":"cpu","problemId":"tactic-synthesis","problemName":"HOL Light Tactic Synthesis","description":"Given a HOL Light goal from s2n-bignum cryptographic proofs, generate a tactic proof that proves the goal. Scored by pass rate (correct proofs / total problems).","metricName":"pass rate","metricDirection":"maximize"},{"competitionId":"geo-bench-2-leaderboard","competitionName":"GEO-Bench 2 Leaderboard","compute":"unknown","problemId":"biomassters-rmse","problemName":"Biomassters RMSE Track","description":"Models are evaluated on RMSE for the Biomassters dataset, with de-normalized scores as per the scale_rmse function.","metricName":"RMSE","metricDirection":"minimize"},{"competitionId":"geo-bench-2-leaderboard","competitionName":"GEO-Bench 2 Leaderboard","compute":"unknown","problemId":"multiclass-jaccard","problemName":"Multiclass Jaccard Index Track","description":"Models are evaluated on multiclass Jaccard index across GEO-Bench datasets using this metric.","metricName":"Multiclass Jaccard Index","metricDirection":"maximize"},{"competitionId":"geo-bench-2-leaderboard","competitionName":"GEO-Bench 2 Leaderboard","compute":"unknown","problemId":"multilabel-f1","problemName":"Multilabel F1 Score Track","description":"Models are evaluated on multilabel F1 score across GEO-Bench datasets using this metric.","metricName":"Multilabel F1 Score","metricDirection":"maximize"},{"competitionId":"geo-bench-2-leaderboard","competitionName":"GEO-Bench 2 Leaderboard","compute":"unknown","problemId":"overall-accuracy","problemName":"Overall Accuracy Track","description":"Models are evaluated on overall accuracy across GEO-Bench datasets using this metric.","metricName":"Overall Accuracy","metricDirection":"maximize"},{"competitionId":"apex-humanoid-parkour","competitionName":"Apex Humanoid Parkour","compute":"cpu","problemId":"humanoid-parkour-course","problemName":"Humanoid Parkour Course","description":"Drive the 12-DoF Unitree G1 through the 51.1 m parkour course; raw_score is the mean over 24 instances with randomized friction and wind. Completions score 1.0 + (max_steps - steps)/max_steps; non-completions score their fraction of course covered.","metricName":"raw_score","metricDirection":"maximize","baseline":0.21},{"competitionId":"clawprobench","competitionName":"ClawProBench","compute":"unknown","problemId":"core","problemName":"Core Profile","description":"Default ranking suite consisting of 26 active scenarios.","metricName":"FinalScore","metricDirection":"maximize"},{"competitionId":"clawprobench","competitionName":"ClawProBench","compute":"unknown","problemId":"intelligence","problemName":"Intelligence Profile","description":"Extended active capability benchmark consisting of 95 active scenarios.","metricName":"FinalScore","metricDirection":"maximize"},{"competitionId":"clawprobench","competitionName":"ClawProBench","compute":"unknown","problemId":"coverage","problemName":"Coverage Profile","description":"Lower-stakes breadth and regression slice consisting of 7 active scenarios.","metricName":"FinalScore","metricDirection":"maximize"},{"competitionId":"clawprobench","competitionName":"ClawProBench","compute":"unknown","problemId":"native","problemName":"Native Profile","description":"Active OpenClaw-native slice only, consisting of 36 active scenarios.","metricName":"FinalScore","metricDirection":"maximize"},{"competitionId":"clawprobench","competitionName":"ClawProBench","compute":"unknown","problemId":"full","problemName":"Full Profile","description":"Union of all active scenarios, consisting of 102 active scenarios.","metricName":"FinalScore","metricDirection":"maximize"},{"competitionId":"squad-explorer","competitionName":"SQuAD","compute":"unknown","problemId":"squad-1-1","problemName":"SQuAD 1.1","description":"The initial version of the Stanford Question Answering Dataset, containing 100,000+ question-answer pairs where the answer is a segment of text.","metricName":"F1","metricDirection":"maximize"},{"competitionId":"squad-explorer","competitionName":"SQuAD","compute":"unknown","problemId":"squad-2-0","problemName":"SQuAD 2.0","description":"SQuAD 2.0 combines the 100,000 questions in SQuAD 1.1 with over 50,000 unanswerable questions written adversarially by crowdworkers.","metricName":"F1","metricDirection":"maximize"},{"competitionId":"reference-kernels","competitionName":"GPU Mode Reference Kernels","compute":"datacenter-gpu","problemId":"causal-conv1d","problemName":"Causal Conv1d","description":"Optimize the 1D causal convolution kernel, commonly used in modern sequence models like Mamba.","metricName":"time","metricDirection":"minimize"},{"competitionId":"reference-kernels","competitionName":"GPU Mode Reference Kernels","compute":"datacenter-gpu","problemId":"gated-deltanet-chunk-fwd-o","problemName":"Gated Deltanet chunk_fwd_o","description":"Optimize the forward pass chunk output kernel for Gated Deltanet.","metricName":"time","metricDirection":"minimize"},{"competitionId":"reference-kernels","competitionName":"GPU Mode Reference Kernels","compute":"datacenter-gpu","problemId":"qr-v2","problemName":"QR Decomposition v2","description":"Optimize QR decomposition with a dedicated Nsight Compute-compatible profile path.","metricName":"time","metricDirection":"minimize"},{"competitionId":"reference-kernels","competitionName":"GPU Mode Reference Kernels","compute":"datacenter-gpu","problemId":"cholesky","problemName":"Cholesky Validation","description":"Optimize Cholesky decomposition with application validation over natural-gradient logistic-regression loops.","metricName":"time","metricDirection":"minimize"},{"competitionId":"reference-kernels","competitionName":"GPU Mode Reference Kernels","compute":"datacenter-gpu","problemId":"eigh","problemName":"Eigh Validation","description":"Optimize symmetric eigenvalue decomposition (eigh) validation kernels.","metricName":"time","metricDirection":"minimize"}]