family_id,draw_rank,paper_title,pdf_url,paper_statement_url,scope_url,formal_coverage,coverage_evidence,comparator_targets,supplied_solution_entry_files,missing_solution_entry_files,written_proof_material,individual_readme_instructions,checker_execution
015,18,Equidistribution of Prime-Degree Torus Packets with Arbitrary Local Type,https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/preprints/Equidistribution-of-Prime-Degree-Torus-Packets-with-Arbitrary-Local-Type-September-24-2026/paper.pdf,https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/preprints/Equidistribution-of-Prime-Degree-Torus-Packets-with-Arbitrary-Local-Type-September-24-2026/build/paper.tex#L103,https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/lean/docs/015.md,main_target,Main target: prime degree at least 5; arbitrary full lattices/local types; discriminant tends to infinity; Haar weak convergence and tightness.,https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/lean/ComparatorChallenges/DukePrimeDegree.lean,,lean/OAI/NumberTheory/DukePrimeDegree/MainUnconditional.lean,True,Citation information only,not_run
024,2,An asymptotic formula for the number of totients,https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/preprints/An-asymptotic-formula-for-the-number-of-totients-September-25-2026/An-asymptotic-formula-for-the-number-of-totients-September-25-2026.pdf,https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/preprints/An-asymptotic-formula-for-the-number-of-totients-September-25-2026/build/source/statements.tex#L45,https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/lean/docs/024.md,main_target,"Main target: explicit positive asymptotic main term, ratio tends to 1, and V(cx)/V(x) tends to c; companion count statements also included.",https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/lean/ComparatorChallenges/TotientAsymptotic.lean | https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/lean/ComparatorChallenges/TotientCompanionZero.lean,,lean/OAI/NumberTheory/TotientAsymptotic/UnconditionalMain.lean | lean/OAI/NumberTheory/TotientAsymptotic/Main.lean,True,Citation information only,not_run
046,7,A projective fourfold with large fundamental group and non-Stein universal cover,https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/preprints/A-projective-fourfold-with-large-fundamental-group-and-non-Stein-universal-cover-October-5-2026/large-fundamental-group-non-stein.pdf,https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/preprints/A-projective-fourfold-with-large-fundamental-group-and-non-Stein-universal-cover-October-5-2026/build/sections/01-introduction.tex#L17,,no_linked_lean,Written construction and proof of a projective fourfold with large fundamental group and non-Stein universal cover; no linked Lean material found.,,,,True,Citation information only,not_run
065,15,Virasoro Constraints under Projectivization,https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/preprints/Virasoro-Constraints-under-Projectivization-October-5-2026/virasoro-constraints-under-projectivization.pdf,https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/preprints/Virasoro-Constraints-under-Projectivization-October-5-2026/build/sections/01-introduction.tex#L36,,no_linked_lean,Written proof that Virasoro constraints pass to projectivization of arbitrary rank-at-least-2 bundles; no linked Lean material found.,,,,True,Citation information only,not_run
082,5,Annular variation of the triangular Hilbert transform at the symmetric point,https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/preprints/Annular-variation-of-the-triangular-Hilbert-transform-at-the-symmetric-point-October-5-2026/annular-variation.pdf,https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/preprints/Annular-variation-of-the-triangular-Hilbert-transform-at-the-symmetric-point-October-5-2026/build/sections/introduction.tex#L27,https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/lean/docs/082.md,supporting_partial,Partial/companion only: maximal hard-truncation estimate. Selected paper main theorem is annular r-variation for every r>2; no such target is supplied.,https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/lean/ComparatorChallenges/TriangularHilbert.lean,lean/OAI/Analysis/TriangularHilbert/Main.lean,,True,Citation information only,not_run
113,9,A Fully Polynomial Randomized Approximation Scheme for Perfect Matchings in General Graphs,https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/preprints/A-Fully-Polynomial-Randomized-Approximation-Scheme-for-Perfect-Matchings-in-General-Graphs-September-23-2026/main.pdf,https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/preprints/A-Fully-Polynomial-Randomized-Approximation-Scheme-for-Perfect-Matchings-in-General-Graphs-September-23-2026/build/main.tex#L132,https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/lean/docs/113.md,main_target,"Main target thm_main asserts FPRAS, polynomial worst-case bit time on every random tape, relative error/failure guarantees and exact zero output. Entropy targets are additional, not substitutes.",https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/lean/ComparatorChallenges/MatchingFPRAS.lean | https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/lean/ComparatorChallenges/MatchingEntropy.lean | https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/lean/ComparatorChallenges/MatchingEntropyBounds.lean | https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/lean/ComparatorChallenges/BinaryMatching.lean | https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/lean/ComparatorChallenges/SingletonLoopMatching.lean | https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/lean/ComparatorChallenges/TriangleFace.lean,lean/OAI/Combinatorics/PerfectMatching/Main.lean | lean/OAI/Computability/MatchingCount/BinarySolve.lean,lean/OAI/Combinatorics/MatchingCount/Main.lean | lean/OAI/Combinatorics/MatchingEntropy/Main.lean | lean/OAI/Computability/LoopMatching/Endpoint.lean | lean/OAI/Combinatorics/TriangleFace/Main.lean,True,Citation information only,not_run
115,13,Exact Uniform Sampling of Contingency Tables with Arbitrary Margins,https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/preprints/Exact-Uniform-Sampling-of-Contingency-Tables-with-Arbitrary-Margins-September-24-2026/main.pdf,https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/preprints/Exact-Uniform-Sampling-of-Contingency-Tables-with-Arbitrary-Margins-September-24-2026/build/sections/introduction.tex#L18,https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/lean/docs/115.md,main_target,"Main targets exactSampling and boundedSampling include exact uniform law, almost-sure termination, polynomial expected bit time and bounded-time approximation.",https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/lean/ComparatorChallenges/ContingencyTables.lean,,lean/OAI/Combinatorics/ContingencyTables/UnconditionalMain.lean,True,Citation information only,not_run
127,4,Average sensitivity of polynomial threshold functions,https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/preprints/Average-Sensitivity-of-Polynomial-Threshold-Functions-September-25-2026/main.pdf,https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/preprints/Average-Sensitivity-of-Polynomial-Threshold-Functions-September-25-2026/build/sections/01-introduction.tex#L20,https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/lean/docs/127.md,main_target,"Main target matches 8*d*sqrt(n) sensitivity bound for multilinear degree <=d, including sign(0)=1.",https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/lean/ComparatorChallenges/GotsmanLinial.lean,lean/OAI/Combinatorics/GotsmanLinial/Main.lean,,True,Citation information only,not_run
148,6,The entropy-rate dimension formula for self-similar measures on the line,https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/preprints/The-entropy-rate-dimension-formula-for-self-similar-measures-on-the-line-September-24-2026/main.pdf,https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/preprints/The-entropy-rate-dimension-formula-for-self-similar-measures-on-the-line-September-24-2026/build/sections/introduction.tex#L78,https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/lean/docs/148.md,main_target,"Main target matches entropy-rate/lower-Hausdorff-dimension formula with positive weights, signed unequal ratios and exact overlaps. Absolute continuity is not claimed.",https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/lean/ComparatorChallenges/SelfSimilar.lean | https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/lean/ComparatorChallenges/SelfSimilarCorollaries.lean,lean/OAI/MeasureTheory/SelfSimilar/Main.lean,lean/OAI/MeasureTheory/SelfSimilar/DimensionCorollaries.lean,True,Citation information only,not_run
154,1,Pointwise Multiple Ergodic Averages for Mixing Transformations,https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/preprints/Pointwise-Multiple-Ergodic-Averages-for-Mixing-Transformations-October-4-2026/multiple-ergodic-averages.pdf,https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/preprints/Pointwise-Multiple-Ergodic-Averages-for-Mixing-Transformations-October-4-2026/build/sections/introduction.tex#L20,,no_linked_lean,Written proof of pointwise multiple ergodic convergence for mixing transformations; no linked Lean material found.,,,,True,Citation information only,not_run
164,10,Monochromatic finite sums and products in the positive integers,https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/preprints/Monochromatic-finite-sums-and-products-in-the-positive-integers-September-23-2026/paper.pdf,https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/preprints/Monochromatic-finite-sums-and-products-in-the-positive-integers-September-23-2026/build/sections/01_introduction.tex#L13,,no_linked_lean,Written proof of monochromatic finite sums and products for every finite set size; no linked Lean material found.,,,,True,Citation information only,not_run
192,20,Unbounded Violations of the Square-Root Degree Bound,https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/preprints/Unbounded-Violations-of-the-Square-Root-Degree-Bound-September-26-2026/Unbounded-Violations-of-the-Square-Root-Degree-Bound-September-26-2026.pdf,https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/preprints/Unbounded-Violations-of-the-Square-Root-Degree-Bound-September-26-2026/build/sections/00-introduction.tex#L23,https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/lean/docs/192.md,main_target,Main target asserts unbounded signed square-root-degree violations and unbounded absolute-coefficient ratios.,https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/lean/ComparatorChallenges/SquareRootDegree.lean,,lean/OAI/Combinatorics/BooleanFunctions/Main.lean,True,Citation information only,not_run
210,19,Foulkes' conjecture for the sixth symmetric power,https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/preprints/Foulkes-Conjecture-for-the-Sixth-Symmetric-Power-September-25-2026/main.pdf,https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/preprints/Foulkes-Conjecture-for-the-Sixth-Symmetric-Power-September-25-2026/build/sections/introduction.tex#L19,https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/lean/docs/210.md,supporting_partial,Partial range: a*(a-1)<=b gives b>=30 at a=6; selected paper claims every b>=6. Cases 6<=b<30 are not covered by this Lean target.,https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/lean/ComparatorChallenges/FoulkesHowe.lean,lean/OAI/RepresentationTheory/FoulkesHowe/Stabilization.lean,,True,Foulkes computational check/run instructions,not_run
215,14,The canonical massive continuum limit of the two-dimensional O(3) model,https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/preprints/The-canonical-massive-continuum-limit-of-the-two-dimensional-O3-model-October-4-2026/massive-continuum-o3.pdf,https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/preprints/The-canonical-massive-continuum-limit-of-the-two-dimensional-O3-model-October-4-2026/build/sections/introduction.tex#L61,https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/lean/docs/215.md,supporting_partial,Supporting/companion only: finite-volume O(n) exponential correlation decay. No canonical interacting O(3) continuum-limit or reconstructed Hamiltonian-gap target.,https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/lean/ComparatorChallenges/ClassicalON.lean,lean/OAI/Probability/ClassicalON/Main.lean,,True,Citation information only,not_run
230,3,An exact Hausdorff gauge for SLE,https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/preprints/An-exact-Hausdorff-gauge-for-SLE-September-25-2026/An-exact-Hausdorff-gauge-for-SLE-September-25-2026.pdf,https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/preprints/An-exact-Hausdorff-gauge-for-SLE-September-25-2026/build/sections/introduction.tex#L38,https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/lean/docs/230.md,supporting_partial,"Supporting component only: positivity for gauges with the explicit small-radius formula. No finite-measure upper bound or finite expectation, and no gauge-existence conclusion in this target.",https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/lean/ComparatorChallenges/SLELowerPositivity.lean,,lean/OAI/Probability/SLE/LowerPositivity.lean,True,Citation information only,not_run
245,17,Weak and strong normalization in pure type systems,https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/preprints/Weak-and-strong-normalization-in-pure-type-systems-September-25-2026/paper.pdf,https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/preprints/Weak-and-strong-normalization-in-pure-type-systems-September-25-2026/build/sections/introduction.tex#L116,https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/lean/docs/245.md,main_target,"Main target: system-wide weak normalization implies strong normalization for arbitrary PTS specifications, including nonfunctional rules and annotated terms.",https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/lean/ComparatorChallenges/TypeSystemNormalization.lean,,lean/OAI/Computability/TypeSystem/Normalization.lean,True,Citation information only,not_run
296,16,Relative generation and the generator problem for finite factors,https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/preprints/Relative-generation-and-the-generator-problem-for-finite-factors-September-23-2026/paper.pdf,https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/preprints/Relative-generation-and-the-generator-problem-for-finite-factors-September-23-2026/build/sections/introduction.tex#L29,https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/lean/docs/296.md,main_target,Main target covers single generation of II1 factors with separable predual; separate RelativeGeneration target covers the dense G-delta relative-generator locus in trace two-topology.,https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/lean/ComparatorChallenges/FactorGeneration.lean | https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/lean/ComparatorChallenges/RelativeGeneration.lean,lean/OAI/Analysis/FactorGeneration/Main.lean,lean/OAI/Analysis/RelativeGeneration/Main.lean,True,Citation information only,not_run
351,11,A closed Ricci flow with bounded scalar curvature and finite-time curvature blowup,https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/preprints/A-closed-Ricci-flow-with-bounded-scalar-curvature-and-finite-time-curvature-blowup-September-24-2026/paper.pdf,https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/preprints/A-closed-Ricci-flow-with-bounded-scalar-curvature-and-finite-time-curvature-blowup-September-24-2026/build/sections/01-introduction.tex#L68,,no_linked_lean,Written proof of closed Ricci-flow example with bounded scalar curvature and finite-time full-curvature blowup; no linked Lean material found.,,,,True,Citation information only,not_run
369,12,Strict hot spots and absence of interior critical points on smooth simply connected planar domains,https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/preprints/Strict-hot-spots-and-absence-of-interior-critical-points-on-smooth-simply-connected-planar-domains-September-24-2026/main.pdf,https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/preprints/Strict-hot-spots-and-absence-of-interior-critical-points-on-smooth-simply-connected-planar-domains-September-24-2026/build/sections/01-introduction.tex#L13,https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/lean/docs/369.md,main_target,"Main target includes nonzero interior gradient and strict boundary-extrema inequalities for every first-positive Neumann eigenfunction, without simplicity requirement.",https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/lean/ComparatorChallenges/HotSpots.lean,,lean/OAI/Analysis/HotSpots/Main.lean,True,Citation information only,not_run
372,8,Global Uniqueness for the Smooth Isotropic Elasticity Inverse Problem,https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/preprints/Global-Uniqueness-for-the-Smooth-Isotropic-Elasticity-Inverse-Problem-September-24-2026/article.pdf,https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/preprints/Global-Uniqueness-for-the-Smooth-Isotropic-Elasticity-Inverse-Problem-September-24-2026/build/sections/introduction.tex#L31,https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/lean/docs/372.md,main_target,Main target asserts Lamé-modulus uniqueness with the stated positivity and smoothness. Boundary pairing uses a variational trace quotient; equivalence to the paper Sobolev trace presentation was not independently proved.,https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/lean/ComparatorChallenges/ElasticityUniqueness.lean,,lean/OAI/MathematicalPhysics/Elasticity/Uniqueness.lean,True,Citation information only,not_run
