family_id,paper_title,coverage,coverage_evidence,paper_statement_url,scope_url,configurations,solution_module_urls,selected_declaration_locations,imported_selected_bodies_not_supplied,implementation_placeholders_found,dependency_completeness,checker_execution
015,Equidistribution of Prime-Degree Torus Packets with Arbitrary Local Type,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/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,https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/lean/ComparatorChallenges/DukePrimeDegree.json,https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/lean/OAI/NumberTheory/DukePrimeDegree/MainUnconditional.lean,OAI.DukePrimeDegree.prime_degree_packet_measure_equidistribution_unconditional: https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/lean/OAI/NumberTheory/DukePrimeDegree/MainUnconditional.lean#L60 | OAI.DukePrimeDegree.prime_degree_packet_measures_tendsto_haar_unconditional: https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/lean/OAI/NumberTheory/DukePrimeDegree/MainUnconditional.lean#L80,,None in supplied text; dependencies not checked,Incomplete,Not run
024,An asymptotic formula for the number of totients,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/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,https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/lean/ComparatorChallenges/TotientAsymptotic.json | https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/lean/ComparatorChallenges/TotientCompanionZero.json,https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/lean/OAI/NumberTheory/TotientAsymptotic/UnconditionalMain.lean | https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/lean/OAI/NumberTheory/TotientAsymptotic/Main.lean,OAI.TotientAsymptotic.totient_asymptotic_formula: https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/lean/OAI/NumberTheory/TotientAsymptotic/UnconditionalMain.lean#L12 | OAI.TotientAsymptotic.weighted_totient_asymptotic: https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/lean/OAI/NumberTheory/TotientAsymptotic/UnconditionalMain.lean#L23 | OAI.TotientAsymptotic.weighted_totient_one_two: https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/lean/OAI/NumberTheory/TotientAsymptotic/UnconditionalMain.lean#L37 | OAI.TotientAsymptotic.coefficient_nonnegative: https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/lean/OAI/NumberTheory/TotientAsymptotic/UnconditionalMain.lean#L44 | OAI.TotientAsymptotic.companion_zero_case: imported body not supplied,OAI.TotientAsymptotic.companion_zero_case,None in supplied text; dependencies not checked,Incomplete,Not run
046,A projective fourfold with large fundamental group and non-Stein universal cover,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.,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,,,,,,Not applicable,Not applicable,Not run
065,Virasoro Constraints under Projectivization,no_linked_lean,Written proof that Virasoro constraints pass to projectivization of arbitrary rank-at-least-2 bundles; no linked Lean material found.,https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/preprints/Virasoro-Constraints-under-Projectivization-October-5-2026/build/sections/01-introduction.tex#L36,,,,,,Not applicable,Not applicable,Not run
082,Annular variation of the triangular Hilbert transform at the symmetric point,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/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,https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/lean/ComparatorChallenges/TriangularHilbert.json,https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/lean/OAI/Analysis/TriangularHilbert/Main.lean,OAI.TriangularHilbert.main_estimate: https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/lean/OAI/Analysis/TriangularHilbert/Main.lean#L38,,None in supplied text; dependencies not checked,Incomplete,Not run
113,A Fully Polynomial Randomized Approximation Scheme for Perfect Matchings in General Graphs,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/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,https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/lean/ComparatorChallenges/MatchingFPRAS.json | https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/lean/ComparatorChallenges/MatchingEntropy.json | https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/lean/ComparatorChallenges/MatchingEntropyBounds.json | https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/lean/ComparatorChallenges/BinaryMatching.json | https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/lean/ComparatorChallenges/SingletonLoopMatching.json | https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/lean/ComparatorChallenges/TriangleFace.json,https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/lean/OAI/Combinatorics/MatchingCount/Main.lean | https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/lean/OAI/Combinatorics/PerfectMatching/Main.lean | https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/lean/OAI/Combinatorics/MatchingEntropy/Main.lean | https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/lean/OAI/Computability/MatchingCount/BinarySolve.lean | https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/lean/OAI/Computability/LoopMatching/Endpoint.lean | https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/lean/OAI/Combinatorics/TriangleFace/Main.lean,OAI.MatchingFPRAS.thm_main: https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/lean/OAI/Combinatorics/MatchingCount/Main.lean#L21 | OAI.MatchingEntropy.entropy_main: https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/lean/OAI/Combinatorics/PerfectMatching/Main.lean#L85 | OAI.MatchingEntropyBounds.Refined.pointwise_entropy: imported body not supplied | OAI.BinaryMatching.deterministic_approximate_counting: https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/lean/OAI/Computability/MatchingCount/BinarySolve.lean#L129 | OAI.LoopMatching.fullEndpoint: https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/lean/OAI/Computability/LoopMatching/Main.lean#L24 | OAI.TriangleFace198.triangle_expansion_face: https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/lean/OAI/Combinatorics/TriangleFace/Main.lean#L51,OAI.MatchingEntropyBounds.Refined.pointwise_entropy,None in supplied text; dependencies not checked,Incomplete,Not run
115,Exact Uniform Sampling of Contingency Tables with Arbitrary Margins,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/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,https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/lean/ComparatorChallenges/ContingencyTables.json,https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/lean/OAI/Combinatorics/ContingencyTables/UnconditionalMain.lean,OAI.ContingencyTables.boundedSampling: https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/lean/OAI/Combinatorics/ContingencyTables/UnconditionalMain.lean#L19 | OAI.ContingencyTables.exactSampling: https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/lean/OAI/Combinatorics/ContingencyTables/UnconditionalMain.lean#L24 | OAI.ContingencyTables.counting: https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/lean/OAI/Combinatorics/ContingencyTables/UnconditionalMain.lean#L29,,None in supplied text; dependencies not checked,Incomplete,Not run
127,Average sensitivity of polynomial threshold functions,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/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,https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/lean/ComparatorChallenges/GotsmanLinial.json,https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/lean/OAI/Combinatorics/GotsmanLinial/Main.lean,OAI.LeanBlast.GotsmanLinial.gotsmanLinialStatement: https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/lean/OAI/Combinatorics/GotsmanLinial/Main.lean#L123,,None in supplied text; dependencies not checked,Incomplete,Not run
148,The entropy-rate dimension formula for self-similar measures on the line,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/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,https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/lean/ComparatorChallenges/SelfSimilar.json | https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/lean/ComparatorChallenges/SelfSimilarCorollaries.json,https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/lean/OAI/MeasureTheory/SelfSimilar/Main.lean | https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/lean/OAI/MeasureTheory/SelfSimilar/DimensionCorollaries.lean,OAI.EntropyRateDimension.entropy_rate_dimension: https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/lean/OAI/MeasureTheory/SelfSimilar/Main.lean#L59 | OAI.EntropyRateDimension.Extensions.homogeneous_dimension_direct: imported body not supplied | OAI.CorSetReference.cor_set: imported body not supplied,OAI.EntropyRateDimension.Extensions.homogeneous_dimension_direct | OAI.CorSetReference.cor_set,None in supplied text; dependencies not checked,Incomplete,Not run
154,Pointwise Multiple Ergodic Averages for Mixing Transformations,no_linked_lean,Written proof of pointwise multiple ergodic convergence for mixing transformations; no linked Lean material found.,https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/preprints/Pointwise-Multiple-Ergodic-Averages-for-Mixing-Transformations-October-4-2026/build/sections/introduction.tex#L20,,,,,,Not applicable,Not applicable,Not run
164,Monochromatic finite sums and products in the positive integers,no_linked_lean,Written proof of monochromatic finite sums and products for every finite set size; no linked Lean material found.,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,,,,,,Not applicable,Not applicable,Not run
192,Unbounded Violations of the Square-Root Degree Bound,main_target,Main target asserts unbounded signed square-root-degree violations and unbounded absolute-coefficient ratios.,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,https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/lean/ComparatorChallenges/SquareRootDegree.json,https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/lean/OAI/Combinatorics/BooleanFunctions/Main.lean,OAI.SquareRootDegree.main: https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/lean/OAI/Combinatorics/BooleanFunctions/Main.lean#L20,,None in supplied text; dependencies not checked,Incomplete,Not run
210,Foulkes' conjecture for the sixth symmetric power,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/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,https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/lean/ComparatorChallenges/FoulkesHowe.json,https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/lean/OAI/RepresentationTheory/FoulkesHowe/Stabilization.lean,OAI.Problem346.canonical_foulkes_howe_surjective: https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/lean/OAI/RepresentationTheory/FoulkesHowe/Stabilization.lean#L15,,None in supplied text; dependencies not checked,Incomplete,Not run
215,The canonical massive continuum limit of the two-dimensional O(3) model,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/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,https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/lean/ComparatorChallenges/ClassicalON.json,https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/lean/OAI/Probability/ClassicalON/Main.lean,OAI.ClassicalON.main: https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/lean/OAI/Probability/ClassicalON/Main.lean#L19,,None in supplied text; dependencies not checked,Incomplete,Not run
230,An exact Hausdorff gauge for SLE,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/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,https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/lean/ComparatorChallenges/SLELowerPositivity.json,https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/lean/OAI/Probability/SLE/LowerPositivity.lean,OAI.SLEExactGauge.sourceLowerMain_proved: https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/lean/OAI/Probability/SLE/LowerPositivity.lean#L60,,None in supplied text; dependencies not checked,Incomplete,Not run
245,Weak and strong normalization in pure type systems,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/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,https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/lean/ComparatorChallenges/TypeSystemNormalization.json,https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/lean/OAI/Computability/TypeSystem/Normalization.lean,OAI.PureTypeSystem.weak_implies_strong: https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/lean/OAI/Computability/TypeSystem/Normalization.lean#L82,,None in supplied text; dependencies not checked,Incomplete,Not run
296,Relative generation and the generator problem for finite factors,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/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,https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/lean/ComparatorChallenges/FactorGeneration.json | https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/lean/ComparatorChallenges/RelativeGeneration.json,https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/lean/OAI/Analysis/FactorGeneration/Main.lean | https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/lean/OAI/Analysis/RelativeGeneration/Main.lean,OAI.Generator.single_generation_of_II1_separable_predual: https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/lean/OAI/Analysis/FactorGeneration/Main.lean#L15 | OAI.RelativeGeneration.main_theorem: https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/lean/OAI/Analysis/RelativeGeneration/Main.lean#L92,,None in supplied text; dependencies not checked,Incomplete,Not run
351,A closed Ricci flow with bounded scalar curvature and finite-time curvature blowup,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.,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,,,,,,Not applicable,Not applicable,Not run
369,Strict hot spots and absence of interior critical points on smooth simply connected planar domains,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/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,https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/lean/ComparatorChallenges/HotSpots.json,https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/lean/OAI/Analysis/HotSpots/Main.lean,OAI.StrictHotSpots.main_theorem: https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/lean/OAI/Analysis/HotSpots/Main.lean#L78,,None in supplied text; dependencies not checked,Incomplete,Not run
372,Global Uniqueness for the Smooth Isotropic Elasticity Inverse Problem,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/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,https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/lean/ComparatorChallenges/ElasticityUniqueness.json,https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/lean/OAI/MathematicalPhysics/Elasticity/Uniqueness.lean,OAI.Elasticity.global_uniqueness: https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/lean/OAI/MathematicalPhysics/Elasticity/Uniqueness.lean#L94,,None in supplied text; dependencies not checked,Incomplete,Not run
