[{"competitionId":"vbench","competitionName":"VBench","compute":"consumer-gpu","problemId":"short-videos","problemName":"Short Videos Track","description":"Evaluation of short video generation (1.6s - 4.0s, 8-24 FPS) across 16 dimensions including temporal quality, frame-wise quality, and text alignment.","metricName":"Total Score","metricDirection":"maximize"},{"competitionId":"vbench","competitionName":"VBench","compute":"consumer-gpu","problemId":"long-videos","problemName":"Long Videos Track","description":"Evaluation of long video generation (10.0s - 40.0s, 8-24 FPS) focusing on temporal consistency and long-term subject consistency.","metricName":"Total Score","metricDirection":"maximize"},{"competitionId":"vbench","competitionName":"VBench","compute":"consumer-gpu","problemId":"vbench-2-0","problemName":"VBench-2.0 (Intrinsic Faithfulness)","description":"Evaluation of advanced capabilities including commonsense reasoning, physics-based realism, human motion, and creative composition across 18 dimensions.","metricName":"Total Score","metricDirection":"maximize"},{"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_bose_gases","problemName":"The energy of dilute Bose gases","description":"Unsolved. Group: formalization-evaluation. Source: S. Fournais and J. P. Solovej, `The energy of dilute Bose gases`, Annals of Math, 192 (3) 2020. Statement taken from https://github.com/ImperialCollegeLondon/An Problem by David Ledvinka.","metricName":"solved","metricDirection":"maximize","baseline":0},{"competitionId":"lean-eval","competitionName":"LeanEval","compute":"none","problemId":"open-annals_bounded_multiplicative_functions","problemName":"Higher uniformity of bounded multiplicative functions in short intervals on average","description":"Unsolved. Group: formalization-evaluation. Source: K. Matomäki, M. Radziwiłł, T. Tao, J. Teräväinen, and T. Ziegler, `Higher uniformity of bounded multiplicative functions in short intervals on average`, Annals  Problem by David Ledvinka.","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_faber_lovasz_conjecture","problemName":"A proof of the Erdős–Faber–Lovász conjecture","description":"Unsolved. Group: formalization-evaluation. Source: D. Y. Kang, T. Kelly, D. Kühn, A. Methuku, and D. Osthus, `A proof of the Erdős–Faber–Lovász conjecture`, Annals of Math, 198 (2) 2023. Statement taken from htt Problem by David Ledvinka.","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_finite_time_singularity","problemName":"Finite-time singularity formation for C^{1,α} solutions to the incompressible Euler equations on ℝ³","description":"Unsolved. Group: formalization-evaluation. Source: T. M. Elgindi, `Finite-time singularity formation for C^{1,α} solutions to the incompressible Euler equations on ℝ³`, Annals of Math, 194 (3) 2021. Statement ta Problem by David Ledvinka.","metricName":"solved","metricDirection":"maximize","baseline":0},{"competitionId":"lean-eval","competitionName":"LeanEval","compute":"none","problemId":"open-annals_good_lt_codes","problemName":"Good Locally Testable Codes","description":"Unsolved. Group: formalization-evaluation. Source: I. Dinur, S. Evra, R. Livne, A. Lubotzky, and S. Mozes, `Good Locally Testable Codes`, Annals of Math, 203 (2) 2026. Statement taken from https://github.com/Imp Problem by Thomas Browning, Katerina Hristova.","metricName":"solved","metricDirection":"maximize","baseline":0},{"competitionId":"lean-eval","competitionName":"LeanEval","compute":"none","problemId":"open-annals_hasse_principle_random_fano","problemName":"The Hasse principle for random Fano hypersurfaces","description":"Unsolved. Group: formalization-evaluation. Source: T. Browning, P. L. Boudec, and W. Sawin, `The Hasse principle for random Fano hypersurfaces`, Annals of Math, 197 (3) 2023. Statement taken from https://github. Problem by Justus Springer.","metricName":"solved","metricDirection":"maximize","baseline":0},{"competitionId":"lean-eval","competitionName":"LeanEval","compute":"none","problemId":"open-annals_integer_multiplication","problemName":"Integer multiplication in time O(n log n)","description":"Unsolved. Group: formalization-evaluation. Source: D. Harvey and J. van der Hoeven, `Integer multiplication in time O(n log n)`, Annals of Math, 193 (2) 2021. Statement taken from https://github.com/ImperialColl 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_motivic_invariants","problemName":"Motivic invariants of birational maps","description":"Unsolved. Group: formalization-evaluation. Source: H.-Y. Lin and E. Shinder, `Motivic invariants of birational maps`, Annals of Math, 199 (1) 2024. Statement taken from https://github.com/ImperialCollegeLondon/A Problem by Justus Springer.","metricName":"solved","metricDirection":"maximize","baseline":0},{"competitionId":"lean-eval","competitionName":"LeanEval","compute":"none","problemId":"open-annals_on_coherence_of_one_relator_groups","problemName":"On the coherence of one-relator groups and their group algebras","description":"Unsolved. Group: formalization-evaluation. Source: A. Jaikin-Zapirain and M. Linton, `On the coherence of one-relator groups and their group algebras`, Annals of Math, 201 (3) 2025. Statement taken from https:// Problem by Katerina Hristova.","metricName":"solved","metricDirection":"maximize","baseline":0},{"competitionId":"lean-eval","competitionName":"LeanEval","compute":"none","problemId":"open-annals_on_property_t","problemName":"On property (T) for Aut(F_n) and SL_n(Z)","description":"Unsolved. Group: formalization-evaluation. Source: M. Kaluba, D. Kielak, and P. W. Nowak, `On property (T) for Aut(F_n) and SL_n(Z)`, Annals of Math, 193 (2) 2021. Statement taken from https://github.com/Imperia Problem by Thomas Browning.","metricName":"solved","metricDirection":"maximize","baseline":0},{"competitionId":"lean-eval","competitionName":"LeanEval","compute":"none","problemId":"open-annals_pointwise_ergodic_theorems","problemName":"Pointwise ergodic theorems for non-conventional bilinear polynomial averages","description":"Unsolved. Group: formalization-evaluation. Source: B. Krause, M. Mirek, and T. Tao, `Pointwise ergodic theorems for non-conventional bilinear polynomial averages`, Annals of Math, 195 (3) 2022. Statement taken f Problem by David Ledvinka.","metricName":"solved","metricDirection":"maximize","baseline":0},{"competitionId":"lean-eval","competitionName":"LeanEval","compute":"none","problemId":"open-annals_rectangular_peg_problem","problemName":"The rectangular peg problem","description":"Unsolved. Group: formalization-evaluation. Source: J. E. Greene and A. Lobb, `The rectangular peg problem`, Annals of Math, 194 (2) 2021. Statement taken from https://github.com/ImperialCollegeLondon/AnnalsChall Problem by Katerina Hristova.","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-annals_wilkies_conjecture","problemName":"Wilkie's conjecture for Pfaffian structures","description":"Unsolved. Group: formalization-evaluation. Source: G. Binyamini, D. Novikov, and B. Zak, `Wilkie's conjecture for Pfaffian structures`, Annals of Math, 199 (2) 2024. Statement taken from https://github.com/Imper Problem by Justus Springer, Mathias Stout.","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-aspherical_integer_homology_four_sphere","problemName":"Existence of an aspherical integer homology 4-sphere","description":"Unsolved. Group: formalization-evaluation. Source: J. G. Ratcliffe and S. T. Tschantz, *On the Davis hyperbolic 4-manifold*, Topology Appl. 111 (2001); see also the discussion of [Kir97, Problem 4.17] in the K3  Problem by Kim Morrison.","metricName":"solved","metricDirection":"maximize","baseline":0},{"competitionId":"lean-eval","competitionName":"LeanEval","compute":"none","problemId":"open-bakerWustholz_linearForms_logs","problemName":"Baker-Wüstholz theorem on linear forms in logarithms","description":"Unsolved. Group: formalization-evaluation. Source: A. Baker, G. Wüstholz, Logarithmic forms and group varieties, J. reine angew. Math. 442 (1993), 19-62. Problem by Ralf Stephan.","metricName":"solved","metricDirection":"maximize","baseline":0},{"competitionId":"lean-eval","competitionName":"LeanEval","compute":"none","problemId":"open-bourgain_polynomial_ergodic","problemName":"Bourgain's polynomial ergodic theorem","description":"Unsolved. Group: formalization-evaluation. Source: J. Bourgain, *Pointwise ergodic theorems for arithmetic sets*, Publ. Math. IHÉS 69 (1989). Knill, *Some fundamental theorems in mathematics*, §173. 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-cdt_linearIndependent","problemName":"Linear independence results of Calegari–Dimitrov–Tang","description":"Unsolved. Group: formalization-evaluation. Source: https://arxiv.org/abs/2408.15403 Problem by Junyan Xu.","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-ckmrv_fourier_interpolation","problemName":"Fourier interpolation in dimensions 8 and 24","description":"Unsolved. Group: formalization-evaluation. Source: H. Cohn, A. Kumar, S. D. Miller, D. Radchenko, and M. Viazovska, 'Universal optimality of the E8 and Leech lattices and interpolation formulas', Ann. of Math. 1 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-direct_summand","problemName":"Direct summand theorem and derived variant","description":"Unsolved. Group: formalization-evaluation. Problem by Junyan Xu.","metricName":"solved","metricDirection":"maximize","baseline":0},{"competitionId":"lean-eval","competitionName":"LeanEval","compute":"none","problemId":"open-einsiedler_katok_lindenstrauss","problemName":"Smallness of exceptional set to Littlewood's 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-equichordal_point_unique","problemName":"Equichordal point theorem (convex curves have a unique equichordal point)","description":"Unsolved. Group: formalization-evaluation. Source: M. R. Rychlik, A complete solution to the equichordal point problem of Fujiwara, Blaschke, Rothe and Weizenböck, Invent. Math. 129 (1997). Listed as §205 in O.  Problem by Kim Morrison.","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-friedlander_iwaniec","problemName":"Friedlander–Iwaniec theorem","description":"Unsolved. Group: formalization-evaluation. Source: Friedlander, John, and Henryk Iwaniec. “The Polynomial X² + Y⁴ Captures Its Primes.” Annals of Mathematics, vol. 148, no. 3, 1998, pp. 945–1040. JSTOR, https:// Problem by Bolton Bailey/Project Numina.","metricName":"solved","metricDirection":"maximize","baseline":0},{"competitionId":"lean-eval","competitionName":"LeanEval","compute":"none","problemId":"open-hSpace_sphere_iff","problemName":"Adams: S^n is an H-space iff n = 0, 1, 3, 7","description":"Unsolved. Group: formalization-evaluation. Source: J. F. Adams, 'On the non-existence of elements of Hopf invariant one', Ann. of Math. 72 (1960), 20-104; J. F. Adams and M. F. Atiyah, 'K-theory and the Hopf inv Problem by Vasily Ilin.","metricName":"solved","metricDirection":"maximize","baseline":0},{"competitionId":"lean-eval","competitionName":"LeanEval","compute":"none","problemId":"open-hilbert_smith_padic_dimension_three","problemName":"No continuous faithful ℤ_p action on a connected 3-manifold (Pardon 2013)","description":"Unsolved. Group: formalization-evaluation. Source: John Pardon, 'The Hilbert-Smith conjecture for three-manifolds', Journal of the American Mathematical Society 26 (2013), no. 3, 879-899, Theorem 1.5. https://do Problem by Jack McCarthy.","metricName":"solved","metricDirection":"maximize","baseline":0},{"competitionId":"lean-eval","competitionName":"LeanEval","compute":"none","problemId":"open-jacobian_challenge_alggeo","problemName":"Jacobian of a smooth proper curve (Merten challenge)","description":"Unsolved. Group: formalization-evaluation. Source: https://leanprover.zulipchat.com/#narrow/stream/583336-Autoformalization/topic/Jacobian%20challenge/near/587802685 Problem by Christian Merten.","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-linnik","problemName":"Linnik's theorem (L = 5.5)","description":"Unsolved. Group: formalization-evaluation. Source: Heath-Brown, D.R. (1992), Zero-Free Regions for Dirichlet L-Functions, and the Least Prime in an Arithmetic Progression. Proceedings of the London Mathematical  Problem by Bolton Bailey/Project Numina.","metricName":"solved","metricDirection":"maximize","baseline":0},{"competitionId":"lean-eval","competitionName":"LeanEval","compute":"none","problemId":"open-mandelbar_not_path_connected","problemName":"Mandelbar (tricorn) is not path-connected (Hubbard–Schleicher)","description":"Unsolved. Group: formalization-evaluation. Source: John H. Hubbard and Dierk Schleicher, *Multicorns are not Path Connected*, arXiv:1209.1753 (2012); published in *Frontiers in Complex Dynamics* (Princeton Unive Problem by Kim Morrison.","metricName":"solved","metricDirection":"maximize","baseline":0},{"competitionId":"lean-eval","competitionName":"LeanEval","compute":"none","problemId":"open-mandelbrot_boundary_dimh","problemName":"Hausdorff dimension of the Mandelbrot boundary (Shishikura)","description":"Unsolved. Group: formalization-evaluation. Source: M. Shishikura, The Hausdorff dimension of the boundary of the Mandelbrot set and Julia sets, Ann. of Math. 147 (1998). Listed as §260 in O. Knill, Some Fundamen Problem by Kim Morrison.","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-milnor_exotic_sphere_seven","problemName":"Milnor's exotic 7-sphere","description":"Unsolved. Group: formalization-evaluation. Source: J. Milnor, On manifolds homeomorphic to the 7-sphere, Ann. of Math. 64 (1956), 399-405. Recorded as a `proof_wanted` in Mathlib/Geometry/Manifold/PoincareConjec Problem by Kim Morrison.","metricName":"solved","metricDirection":"maximize","baseline":0},{"competitionId":"lean-eval","competitionName":"LeanEval","compute":"none","problemId":"open-mostow_rigidity","problemName":"Mostow rigidity","description":"Unsolved. Group: formalization-evaluation. Source: https://en.wikipedia.org/wiki/Mostow_rigidity_theorem#Algebraic_form and Gopal Prasad, *Strong rigidity of ℚ-rank 1 lattices*, Invent. Math. 21 (1973), 255–286. Problem by Junyan Xu.","metricName":"solved","metricDirection":"maximize","baseline":0},{"competitionId":"lean-eval","competitionName":"LeanEval","compute":"none","problemId":"open-newlander_nirenberg","problemName":"Newlander–Nirenberg theorem","description":"Unsolved. Group: formalization-evaluation. Source: A. Newlander and L. Nirenberg, `Complex analytic coordinates in almost complex manifolds`, Annals of Math, 65 (3) 1957, 391-404. 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-pi6_sphere_three_mulEquiv_zmod_twelve","problemName":"pi_6 of the 3-sphere is Z/12","description":"Unsolved. Group: formalization-evaluation. Source: H. Toda, 'Composition Methods in Homotopy Groups of Spheres', Annals of Mathematics Studies 49, Princeton University Press, 1962. The value pi_6(S^3) = Z/12 als Problem by Vasily Ilin.","metricName":"solved","metricDirection":"maximize","baseline":0},{"competitionId":"lean-eval","competitionName":"LeanEval","compute":"none","problemId":"open-pi_sphere_infinite_iff","problemName":"Serre finiteness for homotopy groups of spheres","description":"Unsolved. Group: formalization-evaluation. Source: J.-P. Serre, 'Homologie singuliere des espaces fibres. Applications', Ann. of Math. 54 (1951), 425-505; J.-P. Serre, 'Groupes d'homotopie et classes de groupes  Problem by Vasily Ilin.","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-poincare_high_dim_topological","problemName":"Generalized topological Poincaré conjecture in dimensions ≥ 5 (Smale)","description":"Unsolved. Group: formalization-evaluation. Source: S. Smale, Generalized Poincaré's conjecture in dimensions greater than four, Ann. of Math. 74 (1961), 391-406. Topological case: M. H. A. Newman, The engulfing  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-shafarevich_solvable_galois","problemName":"Shafarevich's theorem on solvable Galois groups","description":"Unsolved. Group: formalization-evaluation. Source: I. R. Shafarevich, 'Construction of fields of algebraic numbers with given solvable Galois group', Izv. Akad. Nauk SSSR Ser. Mat. 18 (1954), no. 6, 525–578, htt Problem by Ryan Smith.","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-space_groups_230","problemName":"230 space groups (Fedorov 1891 / Schoenflies 1891)","description":"Unsolved. Group: formalization-evaluation. Source: E. Fedorov, 'Симметрія правильныхъ системъ фигуръ' (Symmetry of regular systems of figures), Trans. Min. Soc. St. Petersburg 28 (1891) 1–146; A. Schoenflies, *K Problem by Kim Morrison.","metricName":"solved","metricDirection":"maximize","baseline":0},{"competitionId":"lean-eval","competitionName":"LeanEval","compute":"none","problemId":"open-sphere_theorem_differentiable","problemName":"Differentiable sphere theorem (Brendle–Schoen)","description":"Unsolved. Group: formalization-evaluation. Source: S. Brendle & R. Schoen, *Manifolds with 1/4-pinched curvature are space forms*, J. AMS 22 (2009). Knill, *Some fundamental theorems in mathematics*, §121. Problem by Kim Morrison.","metricName":"solved","metricDirection":"maximize","baseline":0},{"competitionId":"lean-eval","competitionName":"LeanEval","compute":"none","problemId":"open-ten_martini_problem","problemName":"Avila-Jitomirskaya Ten Martini Problem","description":"Unsolved. Group: formalization-evaluation. Source: A. Avila and S. Jitomirskaya, 'The Ten Martini Problem', Ann. of Math. 170 (2009), 303-342, https://doi.org/10.4007/annals.2009.170.303. 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-wang_zahl_kakeya_dimH","problemName":"Wang-Zahl: the three-dimensional Kakeya conjecture","description":"Unsolved. Group: formalization-evaluation. Source: H. Wang and J. Zahl, 'Volume estimates for unions of convex sets, and the Kakeya set conjecture in three dimensions', Theorem 1.1, arXiv:2502.17655 (2025), http Problem by Kim Morrison.","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":"lean-eval","competitionName":"LeanEval","compute":"none","problemId":"open-whitney_embedding","problemName":"Whitney embedding theorem (strong form, dimension 2n)","description":"Unsolved. Group: formalization-evaluation. Source: H. Whitney, 'The self-intersections of a smooth n-manifold in 2n-space', Ann. of Math. (2) 45 (1944) 220–246. Earlier 2n+1 form: H. Whitney, 'Differentiable man Problem by Kim Morrison.","metricName":"solved","metricDirection":"maximize","baseline":0},{"competitionId":"agent-anvil-leaderboard","competitionName":"Agent Anvil Public Leaderboard","compute":"none","problemId":"agent_anvil_trace_eval_benchmark","problemName":"Agent Anvil Trace Eval Benchmark","description":"A compact offline benchmark for comparing final-answer-only checks with trace-aware Agent Anvil assertions across tool-use safety scenarios.","metricName":"trace_aware_pass_rate","metricDirection":"maximize"},{"competitionId":"clawprobench","competitionName":"ClawProBench","compute":"consumer-gpu","problemId":"core","problemName":"Core Profile","description":"The default ranking suite consisting of 26 active scenarios.","metricName":"FinalScore","metricDirection":"maximize"},{"competitionId":"clawprobench","competitionName":"ClawProBench","compute":"consumer-gpu","problemId":"intelligence","problemName":"Intelligence Profile","description":"Extended active capability benchmark consisting of 95 active scenarios.","metricName":"FinalScore","metricDirection":"maximize"},{"competitionId":"clawprobench","competitionName":"ClawProBench","compute":"consumer-gpu","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":"consumer-gpu","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":"consumer-gpu","problemId":"full","problemName":"Full Profile","description":"Union of all active scenarios consisting of 102 active scenarios.","metricName":"FinalScore","metricDirection":"maximize"},{"competitionId":"gpu-mode-reference-kernels","competitionName":"GPU Mode Reference Kernels","compute":"datacenter-gpu","problemId":"causal-conv1d","problemName":"Causal Conv1d","description":"Optimize the causal_conv1d kernel from the Helion Kernel Challenge.","metricName":"time","metricDirection":"minimize"},{"competitionId":"gpu-mode-reference-kernels","competitionName":"GPU Mode Reference Kernels","compute":"datacenter-gpu","problemId":"qr-v2","problemName":"QR Decomposition v2","description":"Optimize QR decomposition with Nsight Compute profiling support.","metricName":"time","metricDirection":"minimize"},{"competitionId":"gpu-mode-reference-kernels","competitionName":"GPU Mode Reference Kernels","compute":"datacenter-gpu","problemId":"cholesky","problemName":"Cholesky Validation","description":"Optimize Cholesky factorization evaluated over natural-gradient logistic-regression loops.","metricName":"time","metricDirection":"minimize"},{"competitionId":"gpu-mode-reference-kernels","competitionName":"GPU Mode Reference Kernels","compute":"datacenter-gpu","problemId":"eigh","problemName":"Eigh Validation","description":"Optimize symmetric eigenvalue decomposition (eigh) kernels.","metricName":"time","metricDirection":"minimize"},{"competitionId":"equational-theories-lean-stage2","competitionName":"Mathematics Distillation Challenge — Equational Theories — Stage 2","compute":"unknown","problemId":"solo-track","problemName":"Solo Track","description":"One problem per solver subprocess with a fixed per-problem budget of 3600s wall-clock and 65,536 output tokens per LLM call.","metricName":"score","metricDirection":"maximize"},{"competitionId":"equational-theories-lean-stage2","competitionName":"Mathematics Distillation Challenge — Equational Theories — Stage 2","compute":"unknown","problemId":"marathon-track","problemName":"Marathon Track","description":"N problems per solver subprocess under a compressed global budget (N x 5 minutes wall-clock and N x 32,768 tokens).","metricName":"score","metricDirection":"maximize"},{"competitionId":"geo-bench-2","competitionName":"GEO-Bench 2 Leaderboard","compute":"unknown","problemId":"overall-accuracy","problemName":"Overall Accuracy Track","description":"Evaluation of geospatial models on datasets using Overall Accuracy.","metricName":"accuracy","metricDirection":"maximize"},{"competitionId":"geo-bench-2","competitionName":"GEO-Bench 2 Leaderboard","compute":"unknown","problemId":"multilabel-f1","problemName":"Multilabel F1 Score Track","description":"Evaluation of geospatial models on datasets using Multilabel F1 Score.","metricName":"F1-score","metricDirection":"maximize"},{"competitionId":"geo-bench-2","competitionName":"GEO-Bench 2 Leaderboard","compute":"unknown","problemId":"multiclass-jaccard","problemName":"Multiclass Jaccard Index Track","description":"Evaluation of geospatial models on datasets using Multiclass Jaccard Index (IoU).","metricName":"Jaccard Index","metricDirection":"maximize"},{"competitionId":"geo-bench-2","competitionName":"GEO-Bench 2 Leaderboard","compute":"unknown","problemId":"biomassters-rmse","problemName":"Biomassters RMSE Track","description":"Evaluation of geospatial models on the Biomassters dataset using Root Mean Squared Error.","metricName":"RMSE","metricDirection":"minimize"},{"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":"humanoid-parkour","competitionName":"Humanoid Parkour","compute":"cpu","problemId":"humanoid-parkour-course","problemName":"Humanoid Parkour Course","description":"Drive the Unitree G1 humanoid through the 51m parkour course under randomized wind and friction.","metricName":"raw_score","metricDirection":"maximize","baseline":0.21},{"competitionId":"sutro-problems","competitionName":"Sutro Problems","compute":"datacenter-gpu","problemId":"mnist-medium-3","problemName":"MNIST-medium (3% error target)","description":"Learn from 9x9 images and predict test digits with at most 3% error at the lowest A100 energy.","metricName":"energy","metricDirection":"minimize"},{"competitionId":"sutro-problems","competitionName":"Sutro Problems","compute":"datacenter-gpu","problemId":"mnist-medium-8","problemName":"MNIST-medium (8% error target)","description":"Learn from 9x9 images and predict test digits with at most 8% error at the lowest A100 energy.","metricName":"energy","metricDirection":"minimize"},{"competitionId":"sutro-problems","competitionName":"Sutro Problems","compute":"datacenter-gpu","problemId":"mnist-original","problemName":"MNIST-original (1% test error target)","description":"Learn from original 28x28 images and predict test digits with at most 1% error at the lowest A100 energy.","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.","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.","metricName":"cost","metricDirection":"minimize","baseline":29}]