[{"competitionId":"assetopsbench","competitionName":"AssetOpsBench","compute":"unknown","problemId":"industrial-agent-scenarios","problemName":"Industrial Agent Scenarios","description":"Multi-step end-to-end workflows evaluating AI agents on industrial asset operations and maintenance tasks across 9 asset classes and 141+ scenarios.","metricName":"score","metricDirection":"maximize"},{"competitionId":"alpaca-eval","competitionName":"AlpacaEval","compute":"none","problemId":"alpaca-eval-2","problemName":"AlpacaEval 2.0 (Length-Controlled Win Rate)","description":"Evaluates models using weighted_alpaca_eval_gpt4_turbo as the annotator and gpt4_turbo as the baseline, controlling for length bias.","metricName":"win_rate","metricDirection":"maximize","baseline":50},{"competitionId":"vbench","competitionName":"VBench","compute":"datacenter-gpu","problemId":"short-videos","problemName":"Short Videos Track","description":"Evaluation of short video generation models (1.6-4.0s duration, 8-24 FPS) across temporal quality, frame-wise quality, and text alignment.","metricName":"Total Score","metricDirection":"maximize"},{"competitionId":"vbench","competitionName":"VBench","compute":"datacenter-gpu","problemId":"long-videos","problemName":"Long Videos Track","description":"Evaluation of long video generation models (10.0-40.0s duration, 8-24 FPS) across temporal quality, frame-wise quality, text alignment, and long-range subject consistency.","metricName":"Total Score","metricDirection":"maximize"},{"competitionId":"vbench","competitionName":"VBench","compute":"datacenter-gpu","problemId":"vbench-2-0","problemName":"VBench-2.0 (Intrinsic Faithfulness)","description":"Evaluation of advanced video generation capabilities including commonsense reasoning, physics-based realism, human motion, and creative composition.","metricName":"Total Score","metricDirection":"maximize"},{"competitionId":"vbench","competitionName":"VBench","compute":"datacenter-gpu","problemId":"vbench-i2v","problemName":"VBench-I2V (Image-to-Video)","description":"Evaluation of Image-to-Video (I2V) generation models across video-image alignment (subject/background consistency), camera motion, and video quality.","metricName":"Total Score","metricDirection":"maximize"},{"competitionId":"chess-challenge","competitionName":"Chess Coding Challenge","compute":"none","problemId":"chess-bot","problemName":"Tiny Chess Bot","description":"Create a chess bot in C# within a 1024-token limit.","metricName":"rank","metricDirection":"minimize"},{"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":"polymarket-paper-trader","competitionName":"Polymarket Paper Trader","compute":"none","problemId":"forecast-arena","problemName":"Forecast Arena","description":"AI models and baselines forecast soon-resolving Polymarket binary markets daily without knowing the market price, scored by Brier score against real outcomes.","metricName":"Brier score","metricDirection":"minimize"},{"competitionId":"polymarket-paper-trader","competitionName":"Polymarket Paper Trader","compute":"none","problemId":"paper-trading","problemName":"Paper Trading","description":"AI agents trade $10,000 of paper money against live Polymarket order books, ranked by ROI% with Sharpe ratio as a tiebreaker.","metricName":"ROI","metricDirection":"maximize"},{"competitionId":"putnambench","competitionName":"PutnamBench","compute":"unknown","problemId":"isabelle-proof-only","problemName":"Isabelle (Proof Only)","description":"Proving the problem with the numerical answer written into the theorem statement using Isabelle.","metricName":"score","metricDirection":"maximize"},{"competitionId":"putnambench","competitionName":"PutnamBench","compute":"unknown","problemId":"isabelle-with-answer","problemName":"Isabelle (With Answer)","description":"Producing the numerical answer along with the proof of correctness using Isabelle.","metricName":"score","metricDirection":"maximize"},{"competitionId":"putnambench","competitionName":"PutnamBench","compute":"unknown","problemId":"coq-proof-only","problemName":"Coq (Proof Only)","description":"Proving the problem with the numerical answer written into the theorem statement using Coq.","metricName":"score","metricDirection":"maximize"},{"competitionId":"putnambench","competitionName":"PutnamBench","compute":"unknown","problemId":"coq-with-answer","problemName":"Coq (With Answer)","description":"Producing the numerical answer along with the proof of correctness using Coq.","metricName":"score","metricDirection":"maximize"},{"competitionId":"putnambench","competitionName":"PutnamBench","compute":"unknown","problemId":"lean4-proof-only","problemName":"Lean 4 (Proof Only)","description":"Proving the problem with the numerical answer written into the theorem statement using Lean 4.","metricName":"score","metricDirection":"maximize"},{"competitionId":"putnambench","competitionName":"PutnamBench","compute":"unknown","problemId":"lean4-with-answer","problemName":"Lean 4 (With Answer)","description":"Producing the numerical answer along with the proof of correctness using Lean 4.","metricName":"score","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 problem per solver subprocess with a fixed per-problem budget of 3600s.","metricName":"accuracy","metricDirection":"maximize"},{"competitionId":"equational-theories-lean-stage2","competitionName":"Mathematics Distillation Challenge — Equational Theories — Stage 2","compute":"cpu","problemId":"marathon-track","problemName":"Marathon Track","description":"N problems per solver subprocess with a shared global budget of N x 300s.","metricName":"accuracy","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":"datacenter-gpu","problemId":"mnist-a100-diff3","problemName":"MNIST-a100 (Difficulty 3)","description":"Learn to read digits from 10,000 labeled 9x9 MNIST images, then label 10,000 more, from scratch, on one A100. Difficulty 3 requires error <= 2.70%.","metricName":"time","metricDirection":"minimize"},{"competitionId":"sutro-problems","competitionName":"Sutro Problems","compute":"datacenter-gpu","problemId":"mnist-a100-diff4","problemName":"MNIST-a100 (Difficulty 4)","description":"Learn to read digits from 10,000 labeled 9x9 MNIST images, then label 10,000 more, from scratch, on one A100. Difficulty 4 requires error <= 2.30%.","metricName":"time","metricDirection":"minimize"},{"competitionId":"sutro-problems","competitionName":"Sutro Problems","compute":"datacenter-gpu","problemId":"mnist-a100-diff5","problemName":"MNIST-a100 (Difficulty 5)","description":"Learn to read digits from 10,000 labeled 9x9 MNIST images, then label 10,000 more, from scratch, on one A100. Difficulty 5 requires error <= 1.90%.","metricName":"time","metricDirection":"minimize"},{"competitionId":"sutro-problems","competitionName":"Sutro Problems","compute":"datacenter-gpu","problemId":"mnist-medium-3","problemName":"MNIST-medium (3% error target)","description":"MNIST-medium requires at least 97% mean accuracy on 10,000 training / 10,000 test images of 9x9 pixels.","metricName":"energy","metricDirection":"minimize"},{"competitionId":"sutro-problems","competitionName":"Sutro Problems","compute":"datacenter-gpu","problemId":"mnist-medium-8","problemName":"MNIST-medium (8% error target)","description":"MNIST-medium requires at least 92% mean accuracy on 10,000 training / 10,000 test images of 9x9 pixels.","metricName":"energy","metricDirection":"minimize"},{"competitionId":"sutro-problems","competitionName":"Sutro Problems","compute":"datacenter-gpu","problemId":"mnist-original","problemName":"MNIST-original (1% test error target)","description":"MNIST-original requires at least 99% accuracy on the official 10,000-image test split of 28x28 pixels.","metricName":"energy","metricDirection":"minimize"},{"competitionId":"sutro-problems","competitionName":"Sutro Problems","compute":"datacenter-gpu","problemId":"symmetry-6bit","problemName":"Symmetry (6-bit, 100% target)","description":"Classify a 6-bit pattern as a palindrome (1) or not (0) at the lowest energy on the simplified Bill Dally model (v3 instruction set, 8-bit).","metricName":"cost","metricDirection":"minimize","baseline":20},{"competitionId":"sutro-problems","competitionName":"Sutro Problems","compute":"datacenter-gpu","problemId":"symmetry-8bit","problemName":"Symmetry (8-bit, 100% target)","description":"Classify an 8-bit pattern as a palindrome (1) or not (0) at the lowest energy on the simplified Bill Dally model (v3 instruction set, 8-bit).","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":"s2n-bignum-bench","competitionName":"s2n-bignum-bench","compute":"cpu","problemId":"tactic-synthesis","problemName":"HOL Light Tactic Synthesis","description":"Synthesize HOL Light tactic proofs for cryptographic theorems from AWS s2n-bignum.","metricName":"accuracy","metricDirection":"maximize"},{"competitionId":"geo-bench-2-leaderboard","competitionName":"GEO-Bench Leaderboard","compute":"unknown","problemId":"overall-accuracy","problemName":"Overall Accuracy Track","metricName":"Overall Accuracy","metricDirection":"maximize"},{"competitionId":"geo-bench-2-leaderboard","competitionName":"GEO-Bench Leaderboard","compute":"unknown","problemId":"multilabel-f1","problemName":"Multilabel F1 Score Track","metricName":"Multilabel F1 Score","metricDirection":"maximize"},{"competitionId":"geo-bench-2-leaderboard","competitionName":"GEO-Bench Leaderboard","compute":"unknown","problemId":"multiclass-jaccard","problemName":"Multiclass Jaccard Index Track","metricName":"Multiclass Jaccard Index","metricDirection":"maximize"},{"competitionId":"geo-bench-2-leaderboard","competitionName":"GEO-Bench Leaderboard","compute":"unknown","problemId":"biomassters-rmse","problemName":"Biomassters RMSE Track","metricName":"RMSE","metricDirection":"minimize"},{"competitionId":"apex-humanoid-parkour","competitionName":"Humanoid Parkour","compute":"cpu","problemId":"humanoid-parkour-course","problemName":"Humanoid Parkour Course","description":"Drive a Unitree G1 humanoid through a 51 m parkour course with randomized friction and wind.","metricName":"score","metricDirection":"maximize","baseline":0.21},{"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"},{"competitionId":"medmcqa","competitionName":"MedMCQA","compute":"unknown","problemId":"medmcqa-test-accuracy","problemName":"MedMCQA Test Accuracy","description":"Accuracy on the private test set consisting of AIIMS PG exam MCQs.","metricName":"accuracy","metricDirection":"maximize"}]