# Proof-material availability in a 20-family sample

All **20/20 sampled papers have public manuscript packages listed** (PDF, LaTeX sources, and README). **15/20 belong to families advertising Lean materials**, but this is not a count of fully formalized main results. Only **3/20 selected representatives are explicitly named in the supplied main-result source catalogue**; four other families have a named companion instead. **No proof checker was run.** The exact count with fully covered main results cannot be established from this attachment.

This is a file-inventory and catalogue audit, not an independent mathematical validation. The attachment includes source text for ten repository documents, but only tree metadata for the individual papers and Comparator files. “Available” below means listed as a nonempty repository blob in the supplied snapshot; it does not mean those file contents were downloaded or inspected during this audit.

## Version and sampling

Repository: [openai/math](https://github.com/openai/math/tree/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb), fixed commit `fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb`. Supplied retrieval timestamp: 2026-10-08T10:19:13.206600+00:00. Input SHA-256: `142dce48093da9cbacf49f3c9047b36029fe80e70815ef9e2ffde6a82d7f3360`.

All ten embedded source records match their supplied UTF-8 byte lengths and SHA-256 digests. Both supplied subtree inventories are marked non-truncated. These are internal consistency checks on the user-supplied snapshot, not independent authentication of its relationship to GitHub's commit.

The [manuscript map](https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/CONTENTS.md) parses into 372 distinct families and 719 paper links. Existing family labels span 001–377, with 045, 061, 070, 123 and 163 absent; sampling the integer interval 1–372 would therefore be wrong. We sampled the actual family records in map order, without replacement, using Python 3.12.14 and `random.Random(20261008).sample(families, 20)`. Within each family we chose the first-listed paper, before checking proof availability. It is a representative, not an assumption that it is the only or principal paper. Family membership is the repository's grouping; cross-family overlap was not independently reclassified.

Draw order: 154, 024, 230, 127, 082, 148, 046, 372, 113, 164, 351, 369, 115, 215, 065, 296, 245, 015, 210, 192. No replacement or resampling was performed.

This is a uniform sample of families with deterministic paper selection, not a uniform sample of all 719 manuscripts. Results should not be extrapolated directly to a manuscript-wide formalization rate.

## Counts and evidence levels

| Observable | Count |
|---|---:|
| Listed PDF + at least one TeX source + manuscript README | 20/20 (100%) |
| Family-level Lean link in CONTENTS | 15/20 (75%) |
| Selected representative explicitly in formalization.yaml sources | 3/20 (15%) |
| Other sampled families with a source-listed companion, representative unresolved | 4/20 |
| Remaining family Lean links with unresolved coverage | 8/20 |
| No family Lean link found | 5/20 |
| Lean/Comparator/paper-specific checker executions in this audit | 0 |

The last four coverage categories partition the sample as 3 + 4 + 8 + 5 = 20. The three source-listed papers are catalogue claims, not verified complete proofs. The four companion cases are not counted as coverage of the selected paper. No sampled paper can responsibly be assigned “supporting results only” with certainty from the supplied contents; unresolved coverage must remain unresolved. Zero confirmed supporting-only classifications is not evidence that none exist.

The formalization YAML calls itself a catalogue of papers with a formalized main result, but declares [“Partial progress”](https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/lean/formalization.yaml#L970) and [review status “unchecked”](https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/lean/formalization.yaml#L1778). It has 173 source entries and 200 declaration entries; these are not a complete paper-to-theorem mapping. Omission from this catalogue is not evidence that formal proofs do not exist.

## Per-paper evidence

Paper links and file links below are pinned to the same commit. Each “TeX” link is one example from the listed source files; the JSON evidence file preserves the complete selected-directory inventory, blob hashes and sizes. Individual file contents were not available in the attachment.

| Family | Selected paper | Listed manuscript material | Formal coverage evidence |
|---|---|---|---|
| 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) | PDF; [TeX](https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/preprints/Equidistribution-of-Prime-Degree-Torus-Packets-with-Arbitrary-Local-Type-September-24-2026/build/adelic.tex) (7 .tex files); [README](https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/preprints/Equidistribution-of-Prime-Degree-Torus-Packets-with-Arbitrary-Local-Type-September-24-2026/README.md) | Family Lean link; scope unresolved. [Scope link](https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/lean/docs/015.md). Family Lean link; representative absent from the partial sources list. Main versus supporting scope unresolved. |
| 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) | PDF; [TeX](https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/preprints/An-asymptotic-formula-for-the-number-of-totients-September-25-2026/build/source/collisions.tex) (8 .tex files); [README](https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/preprints/An-asymptotic-formula-for-the-number-of-totients-September-25-2026/README.md) | Family Lean link; scope unresolved. [Scope link](https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/lean/docs/024.md). Family Lean link; representative absent from the partial sources list. Main versus supporting scope unresolved. |
| 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) | PDF; [TeX](https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/preprints/A-projective-fourfold-with-large-fundamental-group-and-non-Stein-universal-cover-October-5-2026/build/figures/arrangement.tex) (12 .tex files); [README](https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/preprints/A-projective-fourfold-with-large-fundamental-group-and-non-Stein-universal-cover-October-5-2026/README.md) | No family Lean link found. [Map](https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/CONTENTS.md#L1233). No family Lean link or exact representative entry found in the supplied catalogue. This is not a repository-wide proof of absence. |
| 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) | PDF; [TeX](https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/preprints/Virasoro-Constraints-under-Projectivization-October-5-2026/build/macros.tex) (11 .tex files); [README](https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/preprints/Virasoro-Constraints-under-Projectivization-October-5-2026/README.md) | No family Lean link found. [Map](https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/CONTENTS.md#L1629). No family Lean link or exact representative entry found in the supplied catalogue. |
| 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) | PDF; [TeX](https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/preprints/Annular-variation-of-the-triangular-Hilbert-transform-at-the-symmetric-point-October-5-2026/build/main.tex) (10 .tex files); [README](https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/preprints/Annular-variation-of-the-triangular-Hilbert-transform-at-the-symmetric-point-October-5-2026/README.md) | Companion listed; representative unresolved. [Scope link](https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/lean/docs/082.md). The catalogue names the companion “The maximal triangular Hilbert transform at the symmetric point”, not this annular-variation paper. A maximal estimate does not by itself establish the advertised r-variation result. |
| 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) | PDF; [TeX](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) (1 .tex files); [README](https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/preprints/A-Fully-Polynomial-Randomized-Approximation-Scheme-for-Perfect-Matchings-in-General-Graphs-September-23-2026/README.md) | Companion listed; representative unresolved. [Scope link](https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/lean/docs/113.md). The catalogue names “Entropy and Face Dimension of the Perfect-Matching Polytope”, not the sampled FPRAS paper. Entropy coverage cannot be counted as verification of the counting algorithm. |
| 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) | PDF; [TeX](https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/preprints/Exact-Uniform-Sampling-of-Contingency-Tables-with-Arbitrary-Margins-September-24-2026/build/figures/repair.tex) (9 .tex files); [README](https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/preprints/Exact-Uniform-Sampling-of-Contingency-Tables-with-Arbitrary-Margins-September-24-2026/README.md) | Family Lean link; scope unresolved. [Scope link](https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/lean/docs/115.md). Family Lean link; exact uniform sampling main-result coverage unresolved. |
| 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) | PDF; [TeX](https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/preprints/Average-Sensitivity-of-Polynomial-Threshold-Functions-September-25-2026/build/figures/grade-coupling.tex) (9 .tex files); [README](https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/preprints/Average-Sensitivity-of-Polynomial-Threshold-Functions-September-25-2026/README.md) | Representative listed; full scope unverified. [Scope link](https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/lean/docs/127.md). [Catalogue](https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/lean/formalization.yaml#L304). Exact representative is listed in the catalogue of papers with a formalized main result (line 304). GotsmanLinial is a corresponding name-based target candidate; its declaration and assumptions were not inspected. |
| 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) | PDF; [TeX](https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/preprints/The-entropy-rate-dimension-formula-for-self-similar-measures-on-the-line-September-24-2026/build/main.tex) (7 .tex files); [README](https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/preprints/The-entropy-rate-dimension-formula-for-self-similar-measures-on-the-line-September-24-2026/README.md) | Representative listed; full scope unverified. [Scope link](https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/lean/docs/148.md). [Catalogue](https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/lean/formalization.yaml#L724). Exact representative is listed in the catalogue of papers with a formalized main result (line 724). SelfSimilar has a catalogue declaration named entropy_rate_dimension; no checking was performed. |
| 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) | PDF; [TeX](https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/preprints/Pointwise-Multiple-Ergodic-Averages-for-Mixing-Transformations-October-4-2026/build/figures/square.tex) (9 .tex files); [README](https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/preprints/Pointwise-Multiple-Ergodic-Averages-for-Mixing-Transformations-October-4-2026/README.md) | No family Lean link found. [Map](https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/CONTENTS.md#L3655). No family Lean link or exact representative entry found in the supplied catalogue. |
| 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) | PDF; [TeX](https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/preprints/Monochromatic-finite-sums-and-products-in-the-positive-integers-September-23-2026/build/main.tex) (10 .tex files); [README](https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/preprints/Monochromatic-finite-sums-and-products-in-the-positive-integers-September-23-2026/README.md) | No family Lean link found. [Map](https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/CONTENTS.md#L3861). No family Lean link or exact representative entry found in the supplied catalogue. |
| 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) | PDF; [TeX](https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/preprints/Unbounded-Violations-of-the-Square-Root-Degree-Bound-September-26-2026/build/bibliography.tex) (9 .tex files); [README](https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/preprints/Unbounded-Violations-of-the-Square-Root-Degree-Bound-September-26-2026/README.md) | Family Lean link; scope unresolved. [Scope link](https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/lean/docs/192.md). Family Lean link; main versus supporting scope unresolved. |
| 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) | PDF; [TeX](https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/preprints/Foulkes-Conjecture-for-the-Sixth-Symmetric-Power-September-25-2026/build/main.tex) (8 .tex files); [README](https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/preprints/Foulkes-Conjecture-for-the-Sixth-Symmetric-Power-September-25-2026/README.md) | Companion listed; representative unresolved. [Scope link](https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/lean/docs/210.md). The catalogue names the companion “Quadratic stabilization of the canonical Foulkes–Howe map”, not this sixth-symmetric-power paper. The sampled paper also has appendix C++ programs, expected outputs and verification/verify_computations.py listed; their contents and coverage were not inspected or executed. |
| 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) | PDF; [TeX](https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/preprints/The-canonical-massive-continuum-limit-of-the-two-dimensional-O3-model-October-4-2026/build/figures/editable.tex) (21 .tex files); [README](https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/preprints/The-canonical-massive-continuum-limit-of-the-two-dimensional-O3-model-October-4-2026/README.md) | Companion listed; representative unresolved. [Scope link](https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/lean/docs/215.md). The catalogue names the companion “Exponential decay in two-dimensional classical O(n) models”. That is not evidence of formalization of the sampled paper’s canonical massive O(3) continuum limit. |
| 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) | PDF; [TeX](https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/preprints/An-exact-Hausdorff-gauge-for-SLE-September-25-2026/build/figures/batch-timeline.tex) (12 .tex files); [README](https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/preprints/An-exact-Hausdorff-gauge-for-SLE-September-25-2026/README.md) | Family Lean link; scope unresolved. [Scope link](https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/lean/docs/230.md). Family Lean link. SLELowerPositivity is a name-based Comparator candidate, but its filename alone cannot establish coverage of the full positive-and-finite exact-gauge result or justify a definite supporting-only classification. |
| 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) | PDF; [TeX](https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/preprints/Weak-and-strong-normalization-in-pure-type-systems-September-25-2026/build/paper.tex) (11 .tex files); [README](https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/preprints/Weak-and-strong-normalization-in-pure-type-systems-September-25-2026/README.md) | Family Lean link; scope unresolved. [Scope link](https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/lean/docs/245.md). Family Lean link; main versus supporting scope unresolved. |
| 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) | PDF; [TeX](https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/preprints/Relative-generation-and-the-generator-problem-for-finite-factors-September-23-2026/build/main.tex) (7 .tex files); [README](https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/preprints/Relative-generation-and-the-generator-problem-for-finite-factors-September-23-2026/README.md) | Representative listed; full scope unverified. [Scope link](https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/lean/docs/296.md). [Catalogue](https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/lean/formalization.yaml#L579). Exact representative is listed in the catalogue of papers with a formalized main result (line 579). The FactorGeneration declaration names single generation; this does not independently establish coverage of the stronger relative-generation assertion also advertised by the family. RelativeGeneration files are listed too, but their contents are absent. |
| 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) | PDF; [TeX](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/figures/drift-cylinder.tex) (10 .tex files); [README](https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/preprints/A-closed-Ricci-flow-with-bounded-scalar-curvature-and-finite-time-curvature-blowup-September-24-2026/README.md) | No family Lean link found. [Map](https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/CONTENTS.md#L8533). No family Lean link or exact representative entry found in the supplied catalogue. |
| 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) | PDF; [TeX](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/figures/boundary-signs.tex) (8 .tex files); [README](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/README.md) | Family Lean link; scope unresolved. [Scope link](https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/lean/docs/369.md). Family Lean link; scope of the strict no-interior-critical-point claim unresolved. |
| 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) | PDF; [TeX](https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/preprints/Global-Uniqueness-for-the-Smooth-Isotropic-Elasticity-Inverse-Problem-September-24-2026/build/main.tex) (7 .tex files); [README](https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/preprints/Global-Uniqueness-for-the-Smooth-Isotropic-Elasticity-Inverse-Problem-September-24-2026/README.md) | Family Lean link; scope unresolved. [Scope link](https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/lean/docs/372.md). Family Lean link; scope of smooth global elasticity uniqueness unresolved. |

## Comparator inventory

These JSON configurations and corresponding `.lean` challenge filenames are present in the supplied Comparator tree. The association to the sampled paper is a **name-based candidate**, not an inspected paper-to-theorem mapping. Challenge statements are not interchangeable with proof implementation files. The supplied YAML names some implementation files, but no implementation-tree inventory or implementation contents were provided.

- Family 015: [DukePrimeDegree.json](https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/lean/ComparatorChallenges/DukePrimeDegree.json).
- Family 024: [TotientAsymptotic.json](https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/lean/ComparatorChallenges/TotientAsymptotic.json), [TotientCompanionZero.json](https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/lean/ComparatorChallenges/TotientCompanionZero.json).
- Family 082: [TriangularHilbert.json](https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/lean/ComparatorChallenges/TriangularHilbert.json).
- Family 113: [MatchingFPRAS.json](https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/lean/ComparatorChallenges/MatchingFPRAS.json), [MatchingEntropy.json](https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/lean/ComparatorChallenges/MatchingEntropy.json).
- Family 115: [ContingencyTables.json](https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/lean/ComparatorChallenges/ContingencyTables.json).
- Family 127: [GotsmanLinial.json](https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/lean/ComparatorChallenges/GotsmanLinial.json).
- Family 148: [SelfSimilar.json](https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/lean/ComparatorChallenges/SelfSimilar.json), [SelfSimilarCorollaries.json](https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/lean/ComparatorChallenges/SelfSimilarCorollaries.json).
- Family 192: [SquareRootDegree.json](https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/lean/ComparatorChallenges/SquareRootDegree.json).
- Family 210: [FoulkesHowe.json](https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/lean/ComparatorChallenges/FoulkesHowe.json).
- Family 215: [ClassicalON.json](https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/lean/ComparatorChallenges/ClassicalON.json).
- Family 230: [SLELowerPositivity.json](https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/lean/ComparatorChallenges/SLELowerPositivity.json).
- Family 245: [TypeSystemNormalization.json](https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/lean/ComparatorChallenges/TypeSystemNormalization.json).
- Family 296: [FactorGeneration.json](https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/lean/ComparatorChallenges/FactorGeneration.json), [RelativeGeneration.json](https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/lean/ComparatorChallenges/RelativeGeneration.json).
- Family 369: [HotSpots.json](https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/lean/ComparatorChallenges/HotSpots.json).
- Family 372: [ElasticityUniqueness.json](https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/lean/ComparatorChallenges/ElasticityUniqueness.json).

The shared [Comparator README](https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/lean/ComparatorChallenges/README.md) explicitly identifies five supporting-only setups: CharacterVarietiesAllSeamsSupport, CartierChartCompactnessSupport, SurfaceConeCandidateSupport, TraceIdealTransportSupport, and HoneycombBridgeMassSupport. They illustrate why challenge presence cannot be counted automatically as a paper's main theorem. They are not substituted into this random sample or added to its numerator.

## Instructions versus execution

The shared instructions were read in full. They require `comparator`, `landrun`, and `lean4export` on PATH, then show commands from `lean/`:

```sh
lake update
lake exe cache get
lake env comparator ComparatorChallenges/QuasiRiemannHypothesis.json
```

These are the repository's example instructions, **not commands executed in this audit** and not evidence about a sampled paper. The [toolchain](https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/lean/lean-toolchain) specifies Lean 4.34.1. The supplied [Lake manifest](https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/lean/lake-manifest.json) records dependency revisions, including mathlib `d13f23b723b8a846827a245b89c10fc7d3f11612`. The [Lean README](https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/lean/README.md) recommends building small portions and documents mmap-related limits. For a reproducible future check, retain and record dependency revisions; do not silently treat any changes from `lake update` as the original frozen environment.

Manuscript-specific README files are listed, but their text was not supplied. The root README describes them as providing citation and build instructions; their individual adequacy was not verified. The Foulkes computational verification script was likewise inventoried, not read or run.

No Lean compiler, Comparator, C++ appendix program, or Python verification script was executed. There are no checker exit codes, success logs, assumption/axiom audits, or proof-gap scans to report. A successful future build would still need a check that the exact formal statement and its assumptions match the paper's advertised result.

## Remaining uncertainty

To finish a content-level coverage audit, obtain the selected papers and their per-family `lean/docs/NNN.md` scope notes, linked configurations and challenge statements, actual proof implementation files, and dependencies. Compare the paper's main statements against the formal declarations, distinguishing weaker statements, additional assumptions, companions, and supporting lemmas. Actual checker execution should be a separate recorded result, with exact revisions, command, exit code, logs, and trusted assumptions.

The defensible answer from this snapshot is **20 listed manuscript packages, 15 family-level Lean links, and no independently checked proofs**. The main-result-versus-supporting-only count remains incompletely determined.
