# Baseline Limitations — 21 July 2026 Status: `PRE-DRAFT DISCLOSURE / REQUIRED IN ANY PUBLIC VERSION` ## Purpose This document states what the current Problem Frontier baseline does not measure, where its classifications can still change and which limitations alter the central thesis rather than merely adding caveats. The baseline is a valid record of a narrow evidence state. It is not a census of AI mathematics or a time series of the global mathematical frontier. ## 1. Scope limitation The strict-core count comes entirely from one AlphaProof Nexus experiment on formalized Erdős problems. It does not cover all mathematical fields, all AI systems, all research-level formal proofs or all human–AI collaborations. Impact: high. Results cannot be generalized to “AI” or “mathematics” without explicitly naming the experiment and cohort. Required wording: “eight retained resolutions among 353 attempted formalized Erdős records in the AlphaProof Nexus experiment.” ## 2. Cohort-selection limitation The 353 attempted problems were selected from questions already available in a formal setting and suitable for the system's workflow. Formalizability, available libraries, statement length and researcher selection may correlate with tractability. Impact: high. The observed yield may not transfer to less structured, literature-heavy or concept-forming research. ## 3. Frozen baseline versus corrected working data `PFT-2026-07-20` contains the original nine-row seed and reproduces from its own immutable inputs. The current event table contains an audit correction that excludes Erdős 846, leaving eight strict-core rows. Impact: high for provenance. Rewriting the frozen snapshot would hide the correction; treating the working table as a second temporal observation would manufacture a trend point. Treatment: publish both states and label the difference as a reclassification. Carry it into the next accepted snapshot's change log. ## 4. Observation-window limitation The corrected public dates place retained events in only two adjacent quarters of 2026. They are clustered releases from one program, not repeated measurements under stable conditions. Impact: fatal to current acceleration claims. Constant, linear, exponential and step-change models cannot be meaningfully compared. ## 5. Publication-date limitation The event date is the first located public proof or result artifact, not necessarily the model's private discovery date, completion date or validation date. Public release can be delayed or batched. Impact: high for quarterly rates. The apparent Q1-to-Q2 increase may reflect disclosure timing. Treatment: call the field `first_public_observation_date` in interpretation, even where the main event table retains the shorter `event_date` label. ## 6. Numerator limitation The Erdős numerator is individually auditable. The OEIS numerator is not. The paper reports 44 successes among 492 attempted mappings, while the public result repository exposes 38 Lean target files representing 37 unique OEIS sequence IDs. Impact: critical. `44/492` remains an author claim and is excluded from the audited event curve. Treatment: do not infer the six absent records or choose between file count and sequence count without the authors' rule. ## 7. Living-registry limitation The Erdős Problems database changes over time and contains several distinct non-settled status classes. The supplied count of 627 completely open records is stale against the pinned revision's 610; the supplied open-like total of 670 does not match the closest explicit component sum of 663. Impact: high. A living registry cannot serve as a fixed depletion denominator without a pinned revision and stable status definition. ## 8. Formal Conjectures membership limitation The Formal Conjectures paper reports 1,029 open research statements. A problem-level table frozen at the matching paper revision has not yet been built. The current repository is an evolving object and cannot substitute for that paper cohort. Impact: high. The largest apparent fixed stock is not yet available for problem-level longitudinal analysis. ## 9. Statement-fidelity limitation Formal verification proves the encoded target. Historical questions may be ambiguous, composite or dependent on conventions not visible in the theorem header. The audit found: - a corrected density interpretation for 125; - natural-, upper- and lower-density separation for 741(i); - a named difference variant rather than all of problem 138; - a weak-density variant with unresolved attribution under problem 26; and - a zero-padding convention needed to read 741(ii) faithfully. Impact: critical. Unchecked statement drift can convert a valid formal proof into a false frontier count. ## 10. Novelty and literature-priority limitation The audit used original sources, curated registry history, public discussion and known independent responses. It was not a systematic search of every relevant journal, monograph, language and equivalent theorem family for all retained rows. Erdős 846 demonstrates the risk: a prior theorem implied the result even though the registry still treated the problem as open. Impact: critical. The eight-row core may shrink under further literature review. Treatment: retain provisional novelty wording for rows without a broad priority audit. ## 11. Mechanical-verification limitation The official repositories' CI results verify the released Lean project at pinned commits. The audit environment does not have Lean's `lake` tool, so the proofs were not rebuilt locally from a clean toolchain. Impact: moderate. Official CI is strong mechanical evidence, but it is not an independent reproducibility environment. Treatment: disclose the official-CI boundary and preserve exact artifact hashes. ## 12. Prose-proof limitation Natural-language PDFs are not guaranteed to be literal explanations of the released Lean artifacts. Some use different constructions; some simplify constants or domains; 12(ii) overstates a quantifier; 741(ii) omits a small infinite-colour step; and 846 omits the hardest converse-collinearity case analysis. Impact: high for readers and comprehension claims. A correct Lean proof does not repair an overclaimed prose theorem, and a short PDF cannot automatically be treated as evidence that humans understand the formal proof. ## 13. Artifact-linkage limitation The AlphaProof Nexus public material contains at least two direct linkage problems: - the 741(i) affirmative upper-density discussion points to the earlier negative natural-density Lean file; and - the 741(ii) paper URL points to the unrelated Erdős 12(ii) file. Impact: moderate to high. Automated extraction from publication links alone would misclassify the proof evidence. Treatment: use the corrected artifact register and keep the defects visible. ## 14. Human-contribution limitation Public descriptions often say that an agent found the proof after humans provided the problem or formal statement. Row-level logs generally do not expose every prompt, retry, lemma hint, selection decision, failed candidate or editorial intervention. Impact: high for autonomy claims. `human_problem_ai_solution` is a categorical description, not a measured percentage of intellectual contribution. Treatment: state only the minimum contribution boundary supported by public evidence. ## 15. Independence and duplicate limitation Independent systems sometimes solved the same problem close together. Those proofs improve confidence and may show different constructions, but they do not remove the same problem twice from a fixed frontier. Impact: moderate. Counting proof events and counting uniquely resolved problems answer different questions. Treatment: retain independent proofs as corroborating events or notes while deduplicating the core problem count. ## 16. Difficulty-measure limitation Problem age is the only computed proxy resembling difficulty, and one retained variant has no defensible source year. Age measures persistence, not depth, importance, abstraction or compute required. Impact: high. The median known age of 32 years cannot support a claim that systems are solving progressively harder mathematics. Treatment: report age descriptively and develop an expert-reviewed difficulty instrument before trend use. ## 17. Verification-lag limitation The pack distinguishes first public observation from later discussion, but it does not yet compute a consistent validation-completion date for every event. Different rows use official CI, curator acceptance, named expert response or published exposition. Impact: moderate. Median verification lag is not currently available. ## 18. Failure-denominator limitation The attempted Erdős and OEIS lists expose cohort membership, but not comparable run-level histories: compute spent, timeouts, partial proofs, retries, human repairs and selection of final artifacts are not public in a consistent form. Impact: high. Success rate cannot be interpreted as research efficiency or probability of solving a randomly selected open problem. ## 19. Compute limitation The workpack has no normalized inference budget, hardware use, wall-clock search time or cost per attempted problem. Impact: high for capability-trend claims. More results may reflect more compute rather than a better algorithm or research method. ## 20. Replenishment limitation No accepted measure counts newly added problems of comparable depth under the same registry and time rules. Variants, formalizations and conjectures created by solutions are not yet classified as replenishment. Impact: fatal to the claim that resolution is outpacing replenishment. Treatment: keep the central title as a question and do not calculate a resolution-to-replenishment ratio. ## 21. Comprehension limitation The workpack has no operational measure of whether experts can understand, teach, simplify or conceptually integrate the proofs. PDF length, proof-term length and omitted details are not sufficient proxies. Impact: fatal to claims that machine mathematics has already escaped human understanding. Treatment: frame comprehension separation as a future scenario until expert study exists. ## 22. Rejection and correction-rate limitation The register preserves some corrections and held cases, but it does not contain a comprehensive denominator of all public or private AI mathematical claims. The Jacobian candidate remains held rather than accepted or rejected. Impact: high. A correction rate computed from the current register would be selection-biased. ## 23. Jacobian-case limitation The three-dimensional Jacobian counterexample candidate is a trigger for the project, not a baseline datapoint. Its provenance, exact hypothesis match, independent expert validation and durable formal status have not passed the publication gate. Impact: critical. It must remain outside the core curve and cannot open a public article as an established resolution. ## 24. Statistical-uncertainty limitation The metric pipeline reports exact counts from the current classification but does not calculate confidence intervals. The larger uncertainty is not random sampling error; it is classification, selection and missing-data uncertainty. Impact: high. Adding conventional error bars would not solve the central measurement problem. Treatment: publish sensitivity classifications and reclassification history before inferential statistics. ## 25. Source-access and preservation limitation The audit depends on repositories, arXiv versions, public forum posts and scanned historical papers. Some sources are living pages; some public evidence may later move or be corrected. Impact: moderate. Without immutable refs, hashes and archived copies, later readers may see a different evidence state. Treatment: preserve commit hashes, versioned paper IDs, capture receipts and content hashes. Do not treat access dates alone as preservation. ## Limitations that currently kill the main measured claim The following are not ordinary caveats. They prevent the current baseline from supporting an empirical claim of imminent frontier depletion: 1. only eight retained strict-core events; 2. only two adjacent quarters of corrected public dates; 3. one system and one selected experiment cohort; 4. no accepted replenishment measure; 5. no second comparable tracker snapshot; 6. incomplete literature-priority review for retained rows; 7. incomplete failure and compute histories; and 8. an unreconciled OEIS numerator. ## Minimum disclosure block for any methods note Any public methods note based on this baseline should include language equivalent to: > This baseline audits one selected AlphaProof Nexus cohort, not mathematics as > a whole. Eight of 353 attempted formalized Erdős records currently pass the > strict full-resolution gate. The count may change under further literature > review. Public dates span only two adjacent quarters and do not support a > trend. The reported 44-of-492 OEIS numerator cannot yet be reproduced from > the 38 public result files. No comparable problem-replenishment series or > compute-normalized failure history exists. ## Editorial consequence The limitations do not make the project empty. They change the publishable finding. The current result is not that AI is running out of problems. It is that a credible measurement system must distinguish proof validity, statement fidelity, novelty, unique-problem counting, publication chronology and moving denominators—and that applying those distinctions already changed the headline count.