# Final material evidence table

Fixed commit: `fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb`. Same 20 family representatives, seed `20261008`; no resampling. All 20 have PDF and TeX written proof material. All checker statuses are **not run**.

Main-result coverage is static correspondence between the advertised paper statement, scope note and formal target. It is not verified proof correctness. Linked solution modules are now supplied for all 23 configurations. All 24 supplied OAI implementation files were scanned after removing comments and strings: no `sorry`, `admit`, `sorryAx` tokens or `axiom` declarations were found. This result does not extend to imports.

“Body absent” means a selected declaration is expected through imports but its defining source was not supplied. It is an evidence gap, not proof that the repository contains an implementation hole. Declaration locations were found by textual inspection; namespace resolution and elaboration were not compiler-checked.

| Family / selected paper | Scope and paper evidence | Configuration → supplied solution entry | Selected implementation declarations and remaining evidence gaps |
|---|---|---|---|
| 015. [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) | **Main result**. [Paper theorem](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); [scope note](https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/lean/docs/015.md). Main target: prime degree at least 5; arbitrary full lattices/local types; discriminant tends to infinity; Haar weak convergence and tightness. | [DukePrimeDegree.json](https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/lean/ComparatorChallenges/DukePrimeDegree.json) → [NumberTheory/DukePrimeDegree/MainUnconditional.lean](https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/lean/OAI/NumberTheory/DukePrimeDegree/MainUnconditional.lean) | `OAI.DukePrimeDegree.prime_degree_packet_measure_equidistribution_unconditional`: [body, line 60](https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/lean/OAI/NumberTheory/DukePrimeDegree/MainUnconditional.lean#L60)<br>`OAI.DukePrimeDegree.prime_degree_packet_measures_tendsto_haar_unconditional`: [body, line 80](https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/lean/OAI/NumberTheory/DukePrimeDegree/MainUnconditional.lean#L80)<br>Imported dependency tree incomplete; checker not run. |
| 024. [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) | **Main result**. [Paper theorem](https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/preprints/An-asymptotic-formula-for-the-number-of-totients-September-25-2026/build/source/statements.tex#L45); [scope note](https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/lean/docs/024.md). Main target: explicit positive asymptotic main term, ratio tends to 1, and V(cx)/V(x) tends to c; companion count statements also included. | [TotientAsymptotic.json](https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/lean/ComparatorChallenges/TotientAsymptotic.json) → [NumberTheory/TotientAsymptotic/UnconditionalMain.lean](https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/lean/OAI/NumberTheory/TotientAsymptotic/UnconditionalMain.lean)<br>[TotientCompanionZero.json](https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/lean/ComparatorChallenges/TotientCompanionZero.json) → [NumberTheory/TotientAsymptotic/Main.lean](https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/lean/OAI/NumberTheory/TotientAsymptotic/Main.lean) | `OAI.TotientAsymptotic.totient_asymptotic_formula`: [body, line 12](https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/lean/OAI/NumberTheory/TotientAsymptotic/UnconditionalMain.lean#L12)<br>`OAI.TotientAsymptotic.weighted_totient_asymptotic`: [body, line 23](https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/lean/OAI/NumberTheory/TotientAsymptotic/UnconditionalMain.lean#L23)<br>`OAI.TotientAsymptotic.weighted_totient_one_two`: [body, line 37](https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/lean/OAI/NumberTheory/TotientAsymptotic/UnconditionalMain.lean#L37)<br>`OAI.TotientAsymptotic.coefficient_nonnegative`: [body, line 44](https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/lean/OAI/NumberTheory/TotientAsymptotic/UnconditionalMain.lean#L44)<br>`OAI.TotientAsymptotic.companion_zero_case`: **imported body not supplied**<br>Imported dependency tree incomplete; checker not run. |
| 046. [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) | **No linked Lean found**. [Paper theorem](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). Written construction and proof of a projective fourfold with large fundamental group and non-Stein universal cover; no linked Lean material found. | Not applicable | Written proof supplied; no linked Lean module found. |
| 065. [Virasoro Constraints under Projectivization](https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/preprints/Virasoro-Constraints-under-Projectivization-October-5-2026/virasoro-constraints-under-projectivization.pdf) | **No linked Lean found**. [Paper theorem](https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/preprints/Virasoro-Constraints-under-Projectivization-October-5-2026/build/sections/01-introduction.tex#L36). Written proof that Virasoro constraints pass to projectivization of arbitrary rank-at-least-2 bundles; no linked Lean material found. | Not applicable | Written proof supplied; no linked Lean module found. |
| 082. [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) | **Supporting / partial only**. [Paper theorem](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); [scope note](https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/lean/docs/082.md). Partial/companion only: maximal hard-truncation estimate. Selected paper main theorem is annular r-variation for every r>2; no such target is supplied. | [TriangularHilbert.json](https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/lean/ComparatorChallenges/TriangularHilbert.json) → [Analysis/TriangularHilbert/Main.lean](https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/lean/OAI/Analysis/TriangularHilbert/Main.lean) | `OAI.TriangularHilbert.main_estimate`: [body, line 38](https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/lean/OAI/Analysis/TriangularHilbert/Main.lean#L38)<br>Imported dependency tree incomplete; checker not run. |
| 113. [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) | **Main result**. [Paper theorem](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); [scope note](https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/lean/docs/113.md). 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. | [MatchingFPRAS.json](https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/lean/ComparatorChallenges/MatchingFPRAS.json) → [Combinatorics/MatchingCount/Main.lean](https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/lean/OAI/Combinatorics/MatchingCount/Main.lean)<br>[MatchingEntropy.json](https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/lean/ComparatorChallenges/MatchingEntropy.json) → [Combinatorics/PerfectMatching/Main.lean](https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/lean/OAI/Combinatorics/PerfectMatching/Main.lean)<br>[MatchingEntropyBounds.json](https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/lean/ComparatorChallenges/MatchingEntropyBounds.json) → [Combinatorics/MatchingEntropy/Main.lean](https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/lean/OAI/Combinatorics/MatchingEntropy/Main.lean)<br>[BinaryMatching.json](https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/lean/ComparatorChallenges/BinaryMatching.json) → [Computability/MatchingCount/BinarySolve.lean](https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/lean/OAI/Computability/MatchingCount/BinarySolve.lean)<br>[SingletonLoopMatching.json](https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/lean/ComparatorChallenges/SingletonLoopMatching.json) → [Computability/LoopMatching/Endpoint.lean](https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/lean/OAI/Computability/LoopMatching/Endpoint.lean)<br>[TriangleFace.json](https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/lean/ComparatorChallenges/TriangleFace.json) → [Combinatorics/TriangleFace/Main.lean](https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/lean/OAI/Combinatorics/TriangleFace/Main.lean) | `OAI.MatchingFPRAS.thm_main`: [body, line 21](https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/lean/OAI/Combinatorics/MatchingCount/Main.lean#L21)<br>`OAI.MatchingEntropy.entropy_main`: [body, line 85](https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/lean/OAI/Combinatorics/PerfectMatching/Main.lean#L85)<br>`OAI.MatchingEntropyBounds.Refined.pointwise_entropy`: **imported body not supplied**<br>`OAI.BinaryMatching.deterministic_approximate_counting`: [body, line 129](https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/lean/OAI/Computability/MatchingCount/BinarySolve.lean#L129)<br>`OAI.LoopMatching.fullEndpoint`: [body, line 24](https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/lean/OAI/Computability/LoopMatching/Main.lean#L24)<br>`OAI.TriangleFace198.triangle_expansion_face`: [body, line 51](https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/lean/OAI/Combinatorics/TriangleFace/Main.lean#L51)<br>Imported dependency tree incomplete; checker not run. |
| 115. [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) | **Main result**. [Paper theorem](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); [scope note](https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/lean/docs/115.md). Main targets exactSampling and boundedSampling include exact uniform law, almost-sure termination, polynomial expected bit time and bounded-time approximation. | [ContingencyTables.json](https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/lean/ComparatorChallenges/ContingencyTables.json) → [Combinatorics/ContingencyTables/UnconditionalMain.lean](https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/lean/OAI/Combinatorics/ContingencyTables/UnconditionalMain.lean) | `OAI.ContingencyTables.boundedSampling`: [body, line 19](https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/lean/OAI/Combinatorics/ContingencyTables/UnconditionalMain.lean#L19)<br>`OAI.ContingencyTables.exactSampling`: [body, line 24](https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/lean/OAI/Combinatorics/ContingencyTables/UnconditionalMain.lean#L24)<br>`OAI.ContingencyTables.counting`: [body, line 29](https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/lean/OAI/Combinatorics/ContingencyTables/UnconditionalMain.lean#L29)<br>Imported dependency tree incomplete; checker not run. |
| 127. [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) | **Main result**. [Paper theorem](https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/preprints/Average-Sensitivity-of-Polynomial-Threshold-Functions-September-25-2026/build/sections/01-introduction.tex#L20); [scope note](https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/lean/docs/127.md). Main target matches 8*d*sqrt(n) sensitivity bound for multilinear degree <=d, including sign(0)=1. | [GotsmanLinial.json](https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/lean/ComparatorChallenges/GotsmanLinial.json) → [Combinatorics/GotsmanLinial/Main.lean](https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/lean/OAI/Combinatorics/GotsmanLinial/Main.lean) | `OAI.LeanBlast.GotsmanLinial.gotsmanLinialStatement`: [body, line 123](https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/lean/OAI/Combinatorics/GotsmanLinial/Main.lean#L123)<br>Imported dependency tree incomplete; checker not run. |
| 148. [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) | **Main result**. [Paper theorem](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); [scope note](https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/lean/docs/148.md). Main target matches entropy-rate/lower-Hausdorff-dimension formula with positive weights, signed unequal ratios and exact overlaps. Absolute continuity is not claimed. | [SelfSimilar.json](https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/lean/ComparatorChallenges/SelfSimilar.json) → [MeasureTheory/SelfSimilar/Main.lean](https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/lean/OAI/MeasureTheory/SelfSimilar/Main.lean)<br>[SelfSimilarCorollaries.json](https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/lean/ComparatorChallenges/SelfSimilarCorollaries.json) → [MeasureTheory/SelfSimilar/DimensionCorollaries.lean](https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/lean/OAI/MeasureTheory/SelfSimilar/DimensionCorollaries.lean) | `OAI.EntropyRateDimension.entropy_rate_dimension`: [body, line 59](https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/lean/OAI/MeasureTheory/SelfSimilar/Main.lean#L59)<br>`OAI.EntropyRateDimension.Extensions.homogeneous_dimension_direct`: **imported body not supplied**<br>`OAI.CorSetReference.cor_set`: **imported body not supplied**<br>Imported dependency tree incomplete; checker not run. |
| 154. [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) | **No linked Lean found**. [Paper theorem](https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/preprints/Pointwise-Multiple-Ergodic-Averages-for-Mixing-Transformations-October-4-2026/build/sections/introduction.tex#L20). Written proof of pointwise multiple ergodic convergence for mixing transformations; no linked Lean material found. | Not applicable | Written proof supplied; no linked Lean module found. |
| 164. [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) | **No linked Lean found**. [Paper theorem](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). Written proof of monochromatic finite sums and products for every finite set size; no linked Lean material found. | Not applicable | Written proof supplied; no linked Lean module found. |
| 192. [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) | **Main result**. [Paper theorem](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); [scope note](https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/lean/docs/192.md). Main target asserts unbounded signed square-root-degree violations and unbounded absolute-coefficient ratios. | [SquareRootDegree.json](https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/lean/ComparatorChallenges/SquareRootDegree.json) → [Combinatorics/BooleanFunctions/Main.lean](https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/lean/OAI/Combinatorics/BooleanFunctions/Main.lean) | `OAI.SquareRootDegree.main`: [body, line 20](https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/lean/OAI/Combinatorics/BooleanFunctions/Main.lean#L20)<br>Imported dependency tree incomplete; checker not run. |
| 210. [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) | **Supporting / partial only**. [Paper theorem](https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/preprints/Foulkes-Conjecture-for-the-Sixth-Symmetric-Power-September-25-2026/build/sections/introduction.tex#L19); [scope note](https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/lean/docs/210.md). 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. | [FoulkesHowe.json](https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/lean/ComparatorChallenges/FoulkesHowe.json) → [RepresentationTheory/FoulkesHowe/Stabilization.lean](https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/lean/OAI/RepresentationTheory/FoulkesHowe/Stabilization.lean) | `OAI.Problem346.canonical_foulkes_howe_surjective`: [body, line 15](https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/lean/OAI/RepresentationTheory/FoulkesHowe/Stabilization.lean#L15)<br>Imported dependency tree incomplete; checker not run. |
| 215. [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) | **Supporting / partial only**. [Paper theorem](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); [scope note](https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/lean/docs/215.md). Supporting/companion only: finite-volume O(n) exponential correlation decay. No canonical interacting O(3) continuum-limit or reconstructed Hamiltonian-gap target. | [ClassicalON.json](https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/lean/ComparatorChallenges/ClassicalON.json) → [Probability/ClassicalON/Main.lean](https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/lean/OAI/Probability/ClassicalON/Main.lean) | `OAI.ClassicalON.main`: [body, line 19](https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/lean/OAI/Probability/ClassicalON/Main.lean#L19)<br>Imported dependency tree incomplete; checker not run. |
| 230. [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) | **Supporting / partial only**. [Paper theorem](https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/preprints/An-exact-Hausdorff-gauge-for-SLE-September-25-2026/build/sections/introduction.tex#L38); [scope note](https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/lean/docs/230.md). 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. | [SLELowerPositivity.json](https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/lean/ComparatorChallenges/SLELowerPositivity.json) → [Probability/SLE/LowerPositivity.lean](https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/lean/OAI/Probability/SLE/LowerPositivity.lean) | `OAI.SLEExactGauge.sourceLowerMain_proved`: [body, line 60](https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/lean/OAI/Probability/SLE/LowerPositivity.lean#L60)<br>Imported dependency tree incomplete; checker not run. |
| 245. [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) | **Main result**. [Paper theorem](https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/preprints/Weak-and-strong-normalization-in-pure-type-systems-September-25-2026/build/sections/introduction.tex#L116); [scope note](https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/lean/docs/245.md). Main target: system-wide weak normalization implies strong normalization for arbitrary PTS specifications, including nonfunctional rules and annotated terms. | [TypeSystemNormalization.json](https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/lean/ComparatorChallenges/TypeSystemNormalization.json) → [Computability/TypeSystem/Normalization.lean](https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/lean/OAI/Computability/TypeSystem/Normalization.lean) | `OAI.PureTypeSystem.weak_implies_strong`: [body, line 82](https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/lean/OAI/Computability/TypeSystem/Normalization.lean#L82)<br>Imported dependency tree incomplete; checker not run. |
| 296. [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) | **Main result**. [Paper theorem](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); [scope note](https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/lean/docs/296.md). 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. | [FactorGeneration.json](https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/lean/ComparatorChallenges/FactorGeneration.json) → [Analysis/FactorGeneration/Main.lean](https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/lean/OAI/Analysis/FactorGeneration/Main.lean)<br>[RelativeGeneration.json](https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/lean/ComparatorChallenges/RelativeGeneration.json) → [Analysis/RelativeGeneration/Main.lean](https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/lean/OAI/Analysis/RelativeGeneration/Main.lean) | `OAI.Generator.single_generation_of_II1_separable_predual`: [body, line 15](https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/lean/OAI/Analysis/FactorGeneration/Main.lean#L15)<br>`OAI.RelativeGeneration.main_theorem`: [body, line 92](https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/lean/OAI/Analysis/RelativeGeneration/Main.lean#L92)<br>Imported dependency tree incomplete; checker not run. |
| 351. [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) | **No linked Lean found**. [Paper theorem](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). Written proof of closed Ricci-flow example with bounded scalar curvature and finite-time full-curvature blowup; no linked Lean material found. | Not applicable | Written proof supplied; no linked Lean module found. |
| 369. [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) | **Main result**. [Paper theorem](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); [scope note](https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/lean/docs/369.md). Main target includes nonzero interior gradient and strict boundary-extrema inequalities for every first-positive Neumann eigenfunction, without simplicity requirement. | [HotSpots.json](https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/lean/ComparatorChallenges/HotSpots.json) → [Analysis/HotSpots/Main.lean](https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/lean/OAI/Analysis/HotSpots/Main.lean) | `OAI.StrictHotSpots.main_theorem`: [body, line 78](https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/lean/OAI/Analysis/HotSpots/Main.lean#L78)<br>Imported dependency tree incomplete; checker not run. |
| 372. [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) | **Main result**. [Paper theorem](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); [scope note](https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/lean/docs/372.md). 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. | [ElasticityUniqueness.json](https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/lean/ComparatorChallenges/ElasticityUniqueness.json) → [MathematicalPhysics/Elasticity/Uniqueness.lean](https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/lean/OAI/MathematicalPhysics/Elasticity/Uniqueness.lean) | `OAI.Elasticity.global_uniqueness`: [body, line 94](https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/lean/OAI/MathematicalPhysics/Elasticity/Uniqueness.lean#L94)<br>Imported dependency tree incomplete; checker not run. |

The four absent selected bodies are:
- `OAI.TotientAsymptotic.companion_zero_case` (family 024, companion zero case).
- `OAI.MatchingEntropyBounds.Refined.pointwise_entropy` (family 113, entropy companion).
- `OAI.EntropyRateDimension.Extensions.homogeneous_dimension_direct` and `OAI.CorSetReference.cor_set` (family 148, dimension corollaries).

These auxiliary-body gaps do not change the main-result scope count: the selected main theorem bodies for those papers are supplied separately. `OAI.LoopMatching.fullEndpoint` is present in the supplied `LoopMatching/Main.lean`, imported by the configured `Endpoint.lean`; it should not be marked missing merely because it is not declared locally in Endpoint.

Of 30 selected declarations, 25 have declaration bodies in the configured entry file, one has its body in another supplied import, and four have no defining body supplied. There are 270 distinct direct OAI imports whose files are absent from the combined attachments. This is a count of unavailable direct dependencies, not a count of proof defects; no transitive or external-library audit was performed.

All 23 challenge files contain specification placeholders. Their `sorry` terms were kept separate from the implementation scan. The permitted-axiom lists in the configurations do not demonstrate that a compiled solution satisfies those lists.

All 15 new records pass their byte-length and SHA-256 checks, and their declared commit matches the earlier package. New attachment SHA-256: `e112b2a78c2acb58ae7b2f38e233842d33926dcf5c96533a2e8ffefb4065c871`. Earlier source package: `4aa791ebc7778974755c8c7701f51a4f8c6a88468962132cc680349a848912e2`. Together they contain 326 records, including 24 OAI implementation files and 23 challenge files.

Nineteen paper READMEs contain citation information only. The Foulkes README documents computational check/run commands, with `--check` explicitly not executing the C++ programs. Shared Comparator/toolchain instructions were available from the original catalogue. No paper-specific computation, compiler, Comparator or axiom check was executed.
