Cheap, abundant machine-checked proofs do not make mathematical knowledge easier to adjudicate; they concentrate difficulty on a tiny pool of experts who must decide whether formal statements actually mean what the informal questions do, widening the gap between certified and socially accepted results.

Main Finding

Machine checking can make derivational verification (kernel-level proof checking) effectively free, producing vast quantities of formally certified artifacts. But this abundance does not eliminate verification work; it relocates and concentrates that work onto non‑mechanizable, expert‑intensive layers—primarily representational fidelity (does the formal statement mean the informal question?) and epistemic significance. Those layers are bounded by the supply of qualified human readers, producing a scarcity of adjudication even while derivational checking is abundant.

Key Points

• Three verification layers
  • L1 — Derivational validity: the kernel checks every inference; mechanizable and cheap (approaches zero cost).
  • L2 — Representational fidelity: whether the formal statement (and its definitions) capture the informal question; requires human expert judgement and is not mechanizable in principle (Fetzer grounding regress).
  • L3 — Epistemic significance: novelty, relevance, framing; social/community judgement, also human‑bound.
• Fetzer / grounding regress: a mechanical check of correspondence between formal and informal requires a formalization of the informal; that returns the problem to the same question, so ultimately a human judgement is inescapable.
• Taxonomy of representational mismatches (audit obligations)
  • T1: quantifier scope displacement
  • T2: reformulation / surrogate statements (declared or not)
  • T3: bespoke definitional substitution (local definitions replacing community‑vetted notions)
  • T4: domain / universe restriction
  • T5: hypothesis satisfied by construction rather than by intended content (hardest to adjudicate)
  • T6: encoding substitution (custom encodings for computational claims)
• Empirical contrast and motivating cases
  • May 2026: OpenAI produced a counterexample to the Erdős unit distance conjecture; five leading mathematicians published a digested, human‑verified writeup the same day — rapid community absorption.
  • Aug 2026: OpenAI released "Ten Advances" with Lean 4 proofs and machine‑checkable certificates. Despite kernel certification (no unproved steps) one listed result (Connes rigidity counterexample) produced an unresolved dispute about whether the formalization meant what it claimed.
• Measurements from openai/ten-proofs (archived 28 Aug 2026)
  • Proof files: ~21.6 MB (20,581,745 bytes)
  • Challenge/statement files (one per headline declaration): ~55.6 KB (56,901 bytes)
  • Ratio: ~379 : 1 (proof : human-audit surface)
  • 12 statement files, 38 theorem statements, 218 local (bespoke) definitions
  • Conclusion: the human readable audit surface per claim is small by size but heavy in expertise requirements (specialists who can both read the formal language and adjudicate domain meaning are rare).
• Economics model (informal)
  • Let g = cost of generating one certified claim, a = cost of competent L2 audit per claim, H = human auditor hours available for the subfield per period.
  • Generation rate ∝ 1/g; audit capability ∝ H/a. Driving g → 0 (cheap generation) without reducing a or increasing H produces a backlog: certified claims outpace adjudication.
• Practical consequence: automation isolates and amplifies the role of rare experts. The fewer incidental L2 checks that occur during human line‑by‑line proof reading, the more consequential each expert judgement becomes.

Data & Methods

• Corpus: openai/ten-proofs repository (main branch), retrieved and archived 28 Aug 2026. Repository metadata (provably agent-reviewed) examined.
• Measurement method:
  • File‑level size tallies from the repository tree (proof module files vs statement/challenge files).
  • Counted number of bespoke definitions in the 12 statement files.
  • Examined individual statements for examples of T3–T6 (e.g., bespoke Turing machines in closest vector problem, bespoke property (T) and ICC definitions in Connes statement).
• Qualitative evidence:
  • Comparative case study: May 2026 (machine output → human digestion → community acceptance) vs Aug 2026 (machine output + formal certificates → unresolved adjudication).
  • Documentary evidence: repository metadata records agent (machine) review rather than human L2 review for the Aug release.
• Reproducibility: the paper reports specific repository paths, sizes and counts; measurements are reproducible from the public tree snapshot referenced.

Implications for AI Economics

• Verification abundance ≠ epistemic throughput: lowering the marginal cost of derivational checking (g) creates a supply surge of certified claims but does not increase the scarce capacity (H) of qualified adjudicators, nor lower per‑claim adjudication cost (a). The bottleneck shifts from verification to adjudication.
• Scarcity of adjudication is a new economic constraint
  • Market implications: as machines flood the literature with formally certified results, competition for the attention of qualified adjudicators will intensify. This raises the value of expert attention (higher implicit/explicit wages, consultancies, bounties) and creates rationing problems.
  • Incentive effects: cheap generation lowers the cost of producing high‑status claims; absent robust adjudication mechanisms, actors may flood fields with machine‑certified but unvetted claims to gain reputational or strategic advantage (noise, confusion, false positives).
• Institutions and market responses likely to emerge
  • Paid audit markets: specialized, credentialed auditors (or audit firms) who are paid to resolve L2/L3 questions. This creates a new service market—formalization audit/interpretation—as a complement to formal proof generation.
  • Certification tiers and provenance disclosure: standardized disclosures (author provenance, whether claim is machine‑generated, whether human L2 audit occurred, local definitions flagged) become valuable signals. The paper proposes a disclosure schema and audit protocol; markets will price reputational assurance.
  • Reputation and platform governance: journals, conferences and repositories may require named human L2 attestations or certified auditor signatures for formal claims to count for tenure/publishing credit; platforms may throttle unaudited machine‑generated claims.
  • Regulatory spillovers: similar issues map to software verification, cryptographic proofs, and regulated decision systems where mechanized proofs or certificates can be manufactured faster than human experts can adjudicate their real‑world mapping and significance.
• Research and public‑goods funding implications
  • Public funding of adjudication capacity (grants to finance deep formal audits) could be socially efficient when the public value of correct adjudication is high.
  • Investment in tooling that reduces a (the per‑claim cost of L2) will help but cannot eliminate the need for expertise. Tools that increase auditor productivity (smart diffing of local definitions vs community standards, automated mismatch detectors guided by the paper’s T1–T6 taxonomy) are likely high‑value complements.
• Risk management
  • Short term: expect confusion and contested claims in high‑value subfields; reliance on opaque machine attestations without human L2 proofs risks propagation of mis‑formalized results.
  • Medium term: emergence of market structures (auditor firms, reputation platforms, mandatory L2 attestations) and of standards (disclosure schemas, taxonomies) that allocate scarce human attention more efficiently.
• Normative policy levers
  • Mandate provenance and disclosure for machine‑generated formal claims (who/what generated, whether human L2 audit occurred, list of local definitions).
  • Fund and credential independent auditors; create incentives (bounties, micro‑payments, publication credit) for L2 adjudication.
  • Support development of tooling that operationalizes the T1–T6 taxonomy to reduce routine adjudication cost and triage auditor attention to the hardest cases (e.g., T5).
  • Encourage repository practices that separate proofs from minimal challenge statements (good engineering practice reduces human reading volume, but must be paired with provenance/disclosure and funded adjudication).

Overall takeaway for AI economics: the major economic constraint produced by high‑throughput formal proof generation is not computational verification but human adjudication. Markets, institutions and policy will need to evolve to allocate and price scarce expert attention, and to create credible signals so that formally certified artifacts are also meaningfully adjudicated.