# Inspectable proof materials in a fixed 20-paper sample

**All 20 papers provide inspectable written proof material. Fifteen have linked Lean comparison material: 11 have targets aligned with their main result, and four have supporting or partial coverage only. Five have no linked Lean material found. No proof checker was executed.** These counts concern material availability and the scope of formal statements, not successful verification or mathematical correctness.

![Scope summary](proof-coverage-summary.png)

## Fixed sample and provenance

The repository is [openai/math at commit fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb](https://github.com/openai/math/tree/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb). We retained the previous sample without substitutions: Python 3.12.14, `random.Random(20261008).sample(families, 20)`, families in CONTENTS order, and the first-listed manuscript from each family. The frame has 372 actual families and 719 manuscripts. Family labels are not contiguous; selection used actual records rather than integers 1–372.

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

This gives each family the same selection probability and prevents papers within one repository-defined family from being counted twice. It does not give every manuscript the same selection probability, independently deduplicate related work across families, or estimate the repository-wide fraction of correct results.

The supplied source package identifies the same commit and retrieval time 2026-10-08T10:23:39.060769+00:00. Its SHA-256 is `4aa791ebc7778974755c8c7701f51a4f8c6a88468962132cc680349a848912e2`. All 311 embedded records passed their supplied size and SHA-256 checks; all 287 records comparable to the earlier catalogue also matched its Git blob SHA-1. This establishes consistency between the attachments, not a fresh independent GitHub retrieval.

The source package contains 20 PDFs, 186 TeX files, 35 Markdown files, 32 Lean files, 24 JSON files and 14 bibliography files. The Markdown files comprise 20 paper READMEs and 15 scope notes. The Lean files comprise 23 Comparator challenge statements and nine OAI implementation entry files. Twenty-three JSON files are Comparator configurations; the remaining JSON is paper support data.

## Method and interpretation

We inspected the actual TeX abstracts and main theorem statements, located proof text in all 20 source packages, read the 15 scope notes, inspected relevant Comparator statement definitions and theorem conclusions, parsed every supplied Comparator configuration, and examined supplied implementation entry files. PDF bytes were decoded and hash-checked; substantive paper-text inspection used TeX, not independently rendered PDFs.

A **main-result target** has the advertised principal conclusion and principal hypotheses in the scope note and the inspected Comparator statement. This is a statement-level assessment. It is not a complete certification of all definitions, encoding equivalences, auxiliary results, transitive proof dependencies, or mathematical correctness.

**Supporting / partial only** means the inspected Lean target is weaker, restricted to part of the parameter range, or concerns a companion result instead of the selected paper's main claim. These four cases retain their full written manuscripts; the restriction applies to the linked Lean scope.

**No linked Lean material found** means none was identified through the supplied manuscript map, formalization catalogue and selected files. It does not assert that no formalization exists anywhere.

| Availability or scope | Papers |
|---|---:|
| Written proof materials: PDF and TeX | 20/20 (100%) |
| Linked scope note, Comparator statement and configuration | 15/20 (75%) |
| Main-result targets | 11/20 (55%) |
| Supporting / partial targets only | 4/20 (20%) |
| No linked Lean material found | 5/20 (25%) |
| Proof-checker executions | 0; all 20 untested |

The 11, four and five categories partition the same 20 representatives. The 15 is their main-plus-supporting total, not 15 independently verified main theorems.

## Evidence for every paper

All links below are pinned. “Paper statement” points directly to the inspected TeX theorem. The accompanying PDF and README are also linked. Every row has written proof material; checker execution is **not run** for every row.

| Family and selected paper | Paper evidence | Lean scope | Assessment |
|---|---|---|---|
| 015. Equidistribution of Prime-Degree Torus Packets with Arbitrary Local Type | [Paper statement](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); [PDF](https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/preprints/Equidistribution-of-Prime-Degree-Torus-Packets-with-Arbitrary-Local-Type-September-24-2026/paper.pdf); [README](https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/preprints/Equidistribution-of-Prime-Degree-Torus-Packets-with-Arbitrary-Local-Type-September-24-2026/README.md) | **Main-result target**. [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. |
| 024. An asymptotic formula for the number of totients | [Paper statement](https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/preprints/An-asymptotic-formula-for-the-number-of-totients-September-25-2026/build/source/statements.tex#L45); [PDF](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); [README](https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/preprints/An-asymptotic-formula-for-the-number-of-totients-September-25-2026/README.md) | **Main-result target**. [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. |
| 046. A projective fourfold with large fundamental group and non-Stein universal cover | [Paper statement](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); [PDF](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); [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 linked Lean material found**. No scope link in supplied map | Written construction and proof of a projective fourfold with large fundamental group and non-Stein universal cover; no linked Lean material found. |
| 065. Virasoro Constraints under Projectivization | [Paper statement](https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/preprints/Virasoro-Constraints-under-Projectivization-October-5-2026/build/sections/01-introduction.tex#L36); [PDF](https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/preprints/Virasoro-Constraints-under-Projectivization-October-5-2026/virasoro-constraints-under-projectivization.pdf); [README](https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/preprints/Virasoro-Constraints-under-Projectivization-October-5-2026/README.md) | **No linked Lean material found**. No scope link in supplied map | Written proof that Virasoro constraints pass to projectivization of arbitrary rank-at-least-2 bundles; no linked Lean material found. |
| 082. Annular variation of the triangular Hilbert transform at the symmetric point | [Paper statement](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); [PDF](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); [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) | **Supporting / partial only**. [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. |
| 113. A Fully Polynomial Randomized Approximation Scheme for Perfect Matchings in General Graphs | [Paper statement](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); [PDF](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); [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) | **Main-result target**. [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. |
| 115. Exact Uniform Sampling of Contingency Tables with Arbitrary Margins | [Paper statement](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); [PDF](https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/preprints/Exact-Uniform-Sampling-of-Contingency-Tables-with-Arbitrary-Margins-September-24-2026/main.pdf); [README](https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/preprints/Exact-Uniform-Sampling-of-Contingency-Tables-with-Arbitrary-Margins-September-24-2026/README.md) | **Main-result target**. [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. |
| 127. Average sensitivity of polynomial threshold functions | [Paper statement](https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/preprints/Average-Sensitivity-of-Polynomial-Threshold-Functions-September-25-2026/build/sections/01-introduction.tex#L20); [PDF](https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/preprints/Average-Sensitivity-of-Polynomial-Threshold-Functions-September-25-2026/main.pdf); [README](https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/preprints/Average-Sensitivity-of-Polynomial-Threshold-Functions-September-25-2026/README.md) | **Main-result target**. [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. |
| 148. The entropy-rate dimension formula for self-similar measures on the line | [Paper statement](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); [PDF](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); [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) | **Main-result target**. [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. |
| 154. Pointwise Multiple Ergodic Averages for Mixing Transformations | [Paper statement](https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/preprints/Pointwise-Multiple-Ergodic-Averages-for-Mixing-Transformations-October-4-2026/build/sections/introduction.tex#L20); [PDF](https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/preprints/Pointwise-Multiple-Ergodic-Averages-for-Mixing-Transformations-October-4-2026/multiple-ergodic-averages.pdf); [README](https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/preprints/Pointwise-Multiple-Ergodic-Averages-for-Mixing-Transformations-October-4-2026/README.md) | **No linked Lean material found**. No scope link in supplied map | Written proof of pointwise multiple ergodic convergence for mixing transformations; no linked Lean material found. |
| 164. Monochromatic finite sums and products in the positive integers | [Paper statement](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); [PDF](https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/preprints/Monochromatic-finite-sums-and-products-in-the-positive-integers-September-23-2026/paper.pdf); [README](https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/preprints/Monochromatic-finite-sums-and-products-in-the-positive-integers-September-23-2026/README.md) | **No linked Lean material found**. No scope link in supplied map | Written proof of monochromatic finite sums and products for every finite set size; no linked Lean material found. |
| 192. Unbounded Violations of the Square-Root Degree Bound | [Paper statement](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); [PDF](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); [README](https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/preprints/Unbounded-Violations-of-the-Square-Root-Degree-Bound-September-26-2026/README.md) | **Main-result target**. [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. |
| 210. Foulkes' conjecture for the sixth symmetric power | [Paper statement](https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/preprints/Foulkes-Conjecture-for-the-Sixth-Symmetric-Power-September-25-2026/build/sections/introduction.tex#L19); [PDF](https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/preprints/Foulkes-Conjecture-for-the-Sixth-Symmetric-Power-September-25-2026/main.pdf); [README](https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/preprints/Foulkes-Conjecture-for-the-Sixth-Symmetric-Power-September-25-2026/README.md) | **Supporting / partial only**. [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. |
| 215. The canonical massive continuum limit of the two-dimensional O(3) model | [Paper statement](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); [PDF](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); [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) | **Supporting / partial only**. [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. |
| 230. An exact Hausdorff gauge for SLE | [Paper statement](https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/preprints/An-exact-Hausdorff-gauge-for-SLE-September-25-2026/build/sections/introduction.tex#L38); [PDF](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); [README](https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/preprints/An-exact-Hausdorff-gauge-for-SLE-September-25-2026/README.md) | **Supporting / partial only**. [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. |
| 245. Weak and strong normalization in pure type systems | [Paper statement](https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/preprints/Weak-and-strong-normalization-in-pure-type-systems-September-25-2026/build/sections/introduction.tex#L116); [PDF](https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/preprints/Weak-and-strong-normalization-in-pure-type-systems-September-25-2026/paper.pdf); [README](https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/preprints/Weak-and-strong-normalization-in-pure-type-systems-September-25-2026/README.md) | **Main-result target**. [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. |
| 296. Relative generation and the generator problem for finite factors | [Paper statement](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); [PDF](https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/preprints/Relative-generation-and-the-generator-problem-for-finite-factors-September-23-2026/paper.pdf); [README](https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/preprints/Relative-generation-and-the-generator-problem-for-finite-factors-September-23-2026/README.md) | **Main-result target**. [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. |
| 351. A closed Ricci flow with bounded scalar curvature and finite-time curvature blowup | [Paper statement](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); [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/paper.pdf); [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 linked Lean material found**. No scope link in supplied map | Written proof of closed Ricci-flow example with bounded scalar curvature and finite-time full-curvature blowup; no linked Lean material found. |
| 369. Strict hot spots and absence of interior critical points on smooth simply connected planar domains | [Paper statement](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); [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/main.pdf); [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) | **Main-result target**. [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. |
| 372. Global Uniqueness for the Smooth Isotropic Elasticity Inverse Problem | [Paper statement](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); [PDF](https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/preprints/Global-Uniqueness-for-the-Smooth-Isotropic-Elasticity-Inverse-Problem-September-24-2026/article.pdf); [README](https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/preprints/Global-Uniqueness-for-the-Smooth-Isotropic-Elasticity-Inverse-Problem-September-24-2026/README.md) | **Main-result target**. [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. |

## Exact targets and supplied implementations

The source notes explicitly link the targets below; these are no longer inferred from filenames. Configuration links specify the solution module and selected declarations. “Missing” means absent from this attachment, not absent from the repository.

**Family 015.**

- [DukePrimeDegree statement](https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/lean/ComparatorChallenges/DukePrimeDegree.lean); [configuration](https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/lean/ComparatorChallenges/DukePrimeDegree.json). `prime_degree_packet_measure_equidistribution_unconditional` ([line 200](https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/lean/ComparatorChallenges/DukePrimeDegree.lean#L200)), `prime_degree_packet_measures_tendsto_haar_unconditional` ([line 215](https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/lean/ComparatorChallenges/DukePrimeDegree.lean#L215)). Solution entry: [lean/OAI/NumberTheory/DukePrimeDegree/MainUnconditional.lean](https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/lean/OAI/NumberTheory/DukePrimeDegree/MainUnconditional.lean) — missing from attachment.

**Family 024.**

- [TotientAsymptotic statement](https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/lean/ComparatorChallenges/TotientAsymptotic.lean); [configuration](https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/lean/ComparatorChallenges/TotientAsymptotic.json). `totient_asymptotic_formula` ([line 118](https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/lean/ComparatorChallenges/TotientAsymptotic.lean#L118)), `weighted_totient_asymptotic` ([line 128](https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/lean/ComparatorChallenges/TotientAsymptotic.lean#L128)), `weighted_totient_one_two` ([line 141](https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/lean/ComparatorChallenges/TotientAsymptotic.lean#L141)), `coefficient_nonnegative` ([line 147](https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/lean/ComparatorChallenges/TotientAsymptotic.lean#L147)). Solution entry: [lean/OAI/NumberTheory/TotientAsymptotic/UnconditionalMain.lean](https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/lean/OAI/NumberTheory/TotientAsymptotic/UnconditionalMain.lean) — missing from attachment.
- [TotientCompanionZero statement](https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/lean/ComparatorChallenges/TotientCompanionZero.lean); [configuration](https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/lean/ComparatorChallenges/TotientCompanionZero.json). `companion_zero_case` ([line 95](https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/lean/ComparatorChallenges/TotientCompanionZero.lean#L95)). Solution entry: [lean/OAI/NumberTheory/TotientAsymptotic/Main.lean](https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/lean/OAI/NumberTheory/TotientAsymptotic/Main.lean) — missing from attachment.

**Family 082.**

- [TriangularHilbert statement](https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/lean/ComparatorChallenges/TriangularHilbert.lean); [configuration](https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/lean/ComparatorChallenges/TriangularHilbert.json). `main_estimate` ([line 50](https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/lean/ComparatorChallenges/TriangularHilbert.lean#L50)). Solution entry: [lean/OAI/Analysis/TriangularHilbert/Main.lean](https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/lean/OAI/Analysis/TriangularHilbert/Main.lean) — supplied.

**Family 113.**

- [MatchingFPRAS statement](https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/lean/ComparatorChallenges/MatchingFPRAS.lean); [configuration](https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/lean/ComparatorChallenges/MatchingFPRAS.json). `thm_main` ([line 105](https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/lean/ComparatorChallenges/MatchingFPRAS.lean#L105)). Solution entry: [lean/OAI/Combinatorics/MatchingCount/Main.lean](https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/lean/OAI/Combinatorics/MatchingCount/Main.lean) — missing from attachment.
- [MatchingEntropy statement](https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/lean/ComparatorChallenges/MatchingEntropy.lean); [configuration](https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/lean/ComparatorChallenges/MatchingEntropy.json). `entropy_main` ([line 58](https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/lean/ComparatorChallenges/MatchingEntropy.lean#L58)). Solution entry: [lean/OAI/Combinatorics/PerfectMatching/Main.lean](https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/lean/OAI/Combinatorics/PerfectMatching/Main.lean) — supplied.
- [MatchingEntropyBounds statement](https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/lean/ComparatorChallenges/MatchingEntropyBounds.lean); [configuration](https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/lean/ComparatorChallenges/MatchingEntropyBounds.json). `Refined.pointwise_entropy` ([line 73](https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/lean/ComparatorChallenges/MatchingEntropyBounds.lean#L73)). Solution entry: [lean/OAI/Combinatorics/MatchingEntropy/Main.lean](https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/lean/OAI/Combinatorics/MatchingEntropy/Main.lean) — missing from attachment.
- [BinaryMatching statement](https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/lean/ComparatorChallenges/BinaryMatching.lean); [configuration](https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/lean/ComparatorChallenges/BinaryMatching.json). `deterministic_approximate_counting` ([line 66](https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/lean/ComparatorChallenges/BinaryMatching.lean#L66)). Solution entry: [lean/OAI/Computability/MatchingCount/BinarySolve.lean](https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/lean/OAI/Computability/MatchingCount/BinarySolve.lean) — supplied.
- [SingletonLoopMatching statement](https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/lean/ComparatorChallenges/SingletonLoopMatching.lean); [configuration](https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/lean/ComparatorChallenges/SingletonLoopMatching.json). `fullEndpoint` ([line 127](https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/lean/ComparatorChallenges/SingletonLoopMatching.lean#L127)). Solution entry: [lean/OAI/Computability/LoopMatching/Endpoint.lean](https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/lean/OAI/Computability/LoopMatching/Endpoint.lean) — missing from attachment.
- [TriangleFace statement](https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/lean/ComparatorChallenges/TriangleFace.lean); [configuration](https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/lean/ComparatorChallenges/TriangleFace.json). `collapse_reattach` ([line 98](https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/lean/ComparatorChallenges/TriangleFace.lean#L98)), `triangle_expansion_face` ([line 169](https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/lean/ComparatorChallenges/TriangleFace.lean#L169)). Solution entry: [lean/OAI/Combinatorics/TriangleFace/Main.lean](https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/lean/OAI/Combinatorics/TriangleFace/Main.lean) — missing from attachment.

**Family 115.**

- [ContingencyTables statement](https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/lean/ComparatorChallenges/ContingencyTables.lean); [configuration](https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/lean/ComparatorChallenges/ContingencyTables.json). `entry_le_row` ([line 69](https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/lean/ComparatorChallenges/ContingencyTables.lean#L69)), `entry_le_total` ([line 74](https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/lean/ComparatorChallenges/ContingencyTables.lean#L74)), `alphabetSize_neZero` ([line 122](https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/lean/ComparatorChallenges/ContingencyTables.lean#L122)), `boundedSampling` ([line 211](https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/lean/ComparatorChallenges/ContingencyTables.lean#L211)), `exactSampling` ([line 214](https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/lean/ComparatorChallenges/ContingencyTables.lean#L214)), `counting` ([line 217](https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/lean/ComparatorChallenges/ContingencyTables.lean#L217)). Solution entry: [lean/OAI/Combinatorics/ContingencyTables/UnconditionalMain.lean](https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/lean/OAI/Combinatorics/ContingencyTables/UnconditionalMain.lean) — missing from attachment.

**Family 127.**

- [GotsmanLinial statement](https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/lean/ComparatorChallenges/GotsmanLinial.lean); [configuration](https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/lean/ComparatorChallenges/GotsmanLinial.json). `gotsmanLinialStatement` ([line 49](https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/lean/ComparatorChallenges/GotsmanLinial.lean#L49)). Solution entry: [lean/OAI/Combinatorics/GotsmanLinial/Main.lean](https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/lean/OAI/Combinatorics/GotsmanLinial/Main.lean) — supplied.

**Family 148.**

- [SelfSimilar statement](https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/lean/ComparatorChallenges/SelfSimilar.lean); [configuration](https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/lean/ComparatorChallenges/SelfSimilar.json). `entropy_rate_dimension` ([line 65](https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/lean/ComparatorChallenges/SelfSimilar.lean#L65)). Solution entry: [lean/OAI/MeasureTheory/SelfSimilar/Main.lean](https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/lean/OAI/MeasureTheory/SelfSimilar/Main.lean) — supplied.
- [SelfSimilarCorollaries statement](https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/lean/ComparatorChallenges/SelfSimilarCorollaries.lean); [configuration](https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/lean/ComparatorChallenges/SelfSimilarCorollaries.json). `homogeneous_dimension_direct` ([line 49](https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/lean/ComparatorChallenges/SelfSimilarCorollaries.lean#L49)), `cor_set` ([line 78](https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/lean/ComparatorChallenges/SelfSimilarCorollaries.lean#L78)). Solution entry: [lean/OAI/MeasureTheory/SelfSimilar/DimensionCorollaries.lean](https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/lean/OAI/MeasureTheory/SelfSimilar/DimensionCorollaries.lean) — missing from attachment.

**Family 192.**

- [SquareRootDegree statement](https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/lean/ComparatorChallenges/SquareRootDegree.lean); [configuration](https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/lean/ComparatorChallenges/SquareRootDegree.json). `main` ([line 57](https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/lean/ComparatorChallenges/SquareRootDegree.lean#L57)). Solution entry: [lean/OAI/Combinatorics/BooleanFunctions/Main.lean](https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/lean/OAI/Combinatorics/BooleanFunctions/Main.lean) — missing from attachment.

**Family 210.**

- [FoulkesHowe statement](https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/lean/ComparatorChallenges/FoulkesHowe.lean); [configuration](https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/lean/ComparatorChallenges/FoulkesHowe.json). `canonical_foulkes_howe_surjective` ([line 42](https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/lean/ComparatorChallenges/FoulkesHowe.lean#L42)). Solution entry: [lean/OAI/RepresentationTheory/FoulkesHowe/Stabilization.lean](https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/lean/OAI/RepresentationTheory/FoulkesHowe/Stabilization.lean) — supplied.

**Family 215.**

- [ClassicalON statement](https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/lean/ComparatorChallenges/ClassicalON.lean); [configuration](https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/lean/ComparatorChallenges/ClassicalON.json). `main` ([line 53](https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/lean/ComparatorChallenges/ClassicalON.lean#L53)). Solution entry: [lean/OAI/Probability/ClassicalON/Main.lean](https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/lean/OAI/Probability/ClassicalON/Main.lean) — supplied.

**Family 230.**

- [SLELowerPositivity statement](https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/lean/ComparatorChallenges/SLELowerPositivity.lean); [configuration](https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/lean/ComparatorChallenges/SLELowerPositivity.json). `sourceLowerMain_proved` ([line 78](https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/lean/ComparatorChallenges/SLELowerPositivity.lean#L78)). Solution entry: [lean/OAI/Probability/SLE/LowerPositivity.lean](https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/lean/OAI/Probability/SLE/LowerPositivity.lean) — missing from attachment.

**Family 245.**

- [TypeSystemNormalization statement](https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/lean/ComparatorChallenges/TypeSystemNormalization.lean); [configuration](https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/lean/ComparatorChallenges/TypeSystemNormalization.json). `weak_implies_strong` ([line 116](https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/lean/ComparatorChallenges/TypeSystemNormalization.lean#L116)). Solution entry: [lean/OAI/Computability/TypeSystem/Normalization.lean](https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/lean/OAI/Computability/TypeSystem/Normalization.lean) — missing from attachment.

**Family 296.**

- [FactorGeneration statement](https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/lean/ComparatorChallenges/FactorGeneration.lean); [configuration](https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/lean/ComparatorChallenges/FactorGeneration.json). `single_generation_of_II1_separable_predual` ([line 41](https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/lean/ComparatorChallenges/FactorGeneration.lean#L41)). Solution entry: [lean/OAI/Analysis/FactorGeneration/Main.lean](https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/lean/OAI/Analysis/FactorGeneration/Main.lean) — supplied.
- [RelativeGeneration statement](https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/lean/ComparatorChallenges/RelativeGeneration.lean); [configuration](https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/lean/ComparatorChallenges/RelativeGeneration.json). `main_theorem` ([line 103](https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/lean/ComparatorChallenges/RelativeGeneration.lean#L103)). Solution entry: [lean/OAI/Analysis/RelativeGeneration/Main.lean](https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/lean/OAI/Analysis/RelativeGeneration/Main.lean) — missing from attachment.

**Family 369.**

- [HotSpots statement](https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/lean/ComparatorChallenges/HotSpots.lean); [configuration](https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/lean/ComparatorChallenges/HotSpots.json). `main_theorem` ([line 49](https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/lean/ComparatorChallenges/HotSpots.lean#L49)). Solution entry: [lean/OAI/Analysis/HotSpots/Main.lean](https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/lean/OAI/Analysis/HotSpots/Main.lean) — missing from attachment.

**Family 372.**

- [ElasticityUniqueness statement](https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/lean/ComparatorChallenges/ElasticityUniqueness.lean); [configuration](https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/lean/ComparatorChallenges/ElasticityUniqueness.json). `global_uniqueness` ([line 103](https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/lean/ComparatorChallenges/ElasticityUniqueness.lean#L103)). Solution entry: [lean/OAI/MathematicalPhysics/Elasticity/Uniqueness.lean](https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/lean/OAI/MathematicalPhysics/Elasticity/Uniqueness.lean) — missing from attachment.


## The four coverage shortfalls

**082, annular variation.** The selected paper's main theorem bounds full annular r-variation for every r>2. The supplied TriangularHilbert target and implementation prove a maximal hard-truncation estimate. A maximal bound is not the full variation theorem, even though both belong to the same family.

**210, sixth-power Foulkes.** The paper states its conclusion for every b≥6. FoulkesHowe assumes b≥a(a−1), which becomes b≥30 at a=6. It therefore covers a restricted range and does not cover 6≤b<30. The scope note explicitly states this exclusion.

**215, O(3) continuum limit.** The selected paper constructs a canonical interacting continuum theory, with convergence and mass-gap assertions. ClassicalON concerns exponential spin-correlation decay on finite lattice graphs. The scope note excludes the infinite-volume limit; finite-volume decay is not the selected continuum-limit result.

**230, SLE exact gauge.** The paper claims existence of a deterministic gauge with positive **finite** measure on every nontrivial positive-time segment, plus finite expected measure in bounded regions. SLELowerPositivity concludes only positivity, conditional on a gauge having a prescribed small-radius formula. It contains neither the finite-measure upper bound nor the finite-expectation conclusion, and does not itself assert existence of such a gauge.

## Files, instructions and execution

The Comparator challenge statements contain `sorry` placeholders. They specify what separate solution modules must establish; they are not completed proofs by themselves. Counting or compiling these challenge files alone would not demonstrate that the paper was proved.

All 23 inspected Comparator configurations permit only `propext`, `Quot.sound`, and `Classical.choice`; all set `enable_nanoda: false`. These are configuration settings, not evidence that the actual solutions passed an axiom check. In particular, the configuration's allowance list cannot replace examination of the compiled solution.

Nine OAI implementation files were supplied. A lexical scan found no `sorry`, `admit`, or `sorryAx` tokens in those files. That observation applies only to these nine files: 23 distinct direct OAI imports are absent. Only eight of the 23 configurations have their exact `solution_module` file supplied. The extra LoopMatching entry file is not the exact module named by its configuration. The attachment is therefore not a complete buildable proof library, and the missing dependencies were not audited.

The shared [Comparator instructions](https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/lean/ComparatorChallenges/README.md) require Comparator, landrun and lean4export, followed by Lake dependency/cache setup and a Comparator invocation. The pinned [Lean toolchain](https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/lean/lean-toolchain) specifies Lean 4.34.1; the [Lake manifest](https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/lean/lake-manifest.json) records dependency revisions. Those documents were inspected in the earlier catalogue and remain applicable to the same commit.

Inspection corrects a possible inference from README presence: **19 of the 20 individual READMEs contain citation information only.** The Foulkes README contains computational verification instructions:
- `python3 -B verification/verify_computations.py --check` checks identities, expected numeric rows, table agreement and numerical bounds; it explicitly does not execute the C++ programs.
- `python3 -B verification/verify_computations.py --run --serial` is documented to compile/run both exact computations and compare their outputs, requiring GNU C++ with signed 128-bit integers and Boost headers.

Neither command was run. The C++ and Python program contents are not included in this new attachment, although their paths were listed in the earlier repository inventory. The written verification instructions and expected data are not execution logs.

No Lean compiler, Comparator, Nanoda, C++ computation, paper verification script or LaTeX build was executed in this audit. Hash validation and plotting are the computations performed here; they are not mathematical proof checking. “Untested” must not be read as “failed.”

## Qualifications

The main-result count is now based on the actual scope notes and statements, rather than membership in the incomplete formalization YAML. This resolves the earlier catalogue-only uncertainty but does not establish 11 successfully checked proofs.

For family 296, both the single-generation and relative-generation statements are represented, but only the single-generation solution entry is supplied. For family 372, the formal target presents boundary data through a variational trace quotient; equivalence to the paper's Sobolev trace-space presentation was not independently proved. More generally, statement correspondence has not been promoted into a comprehensive formalization review.

The reproducible evidence JSON includes main-theorem excerpts, proof-text locators, exact target names, solution-module availability, per-record hashes and the unchanged sample order. The figure shows these descriptive scope categories, with no inferential confidence interval or claim about the truth of the underlying results.
