Proofs after AlephZero: epistemic phase transitions in AI-era mathematics

1Where this starts

The 2022 paper made three claims about how belief in a proof forms: proof networks have the topology (heavy-tailed re-use, α ≈ 2, high modularity) needed for an epistemic phase transition — a jump to near-certainty at realistic per-step error rates; modules act as firewalls that contain doubt; and deduction and abduction must stay balanced, or certainty collapses (the abductive paradox). Two later papers set the AI-era agenda: AlephZero and mathematical experience (DeDeo 2024) predicts automation transforms impasse, error, and aboutness; A correspondence problem for mathematical proof (DeDeo & Duede 2026) argues a formalization justifies a particular proof only if it represents its theorem and tracks its steps — and that AI-era pipelines weaken exactly the causal and explanatory provenance that tracking requires.

Between 2022 and 2026 the object of study changed under the instrument: mathlib passed two million lines; Tao's PFR formalization took three weeks; the Equational Theories Project (ETP) settled all 22,028,942 implications among 4,694 magma laws with humans, ATPs, and LLMs in one repository; AlphaProof reached IMO silver; Gauss finished the sphere-packing formalization in five days and autoformalized the dimension-24 case from the original paper in two. Every one of these projects publishes its full dependency structure. The 2022 methodology can simply be pointed at them.

2New data, two grains

For each of four flagship projects — PFR (teorth/pfr), FLT (ImperialCollegeLondon/FLT), Sphere Packing (human-led repo and Math Inc's AI-completed fork), and Equational Theories (teorth/equational_theories) — two networks were extracted:

• Blueprint graphs (informal grain): nodes are statements in the human-written LaTeX blueprint; edges are the authors' own \uses{} declarations. These are the direct descendants of the hand-coded Euclid/Wiles/Herstein networks of 2022 — with the difference that the community now writes the network itself as a working document.
• Lean declaration graphs (formal grain): nodes are named declarations (theorem/lemma/def …); edges are textual references from one declaration's statement or proof to another. AlphaProof's raw IMO 2024 outputs, human formalizations of the same three problems (J. Myers, mathlib Archive), and AlphaProof Nexus's 2026 research-level corpus (2,494 theorems) were analyzed at the finer intra-proof grain: named-claim networks inside each proof.

Method caveat. Lean graphs here are textual (no compilation), so edges mediated by simp-sets or mathlib intermediaries are missed and suffix-matching admits some noise; absolute edge counts are lower bounds and cross-corpus comparisons are the meaningful quantity. Statistics are computed on largest weakly-connected components; α by discrete Clauset–Shalizi–Newman MLE; belief dynamics by the paper's asymmetric-Ising Glauber model (p_prior = 0.75, 10 sweeps); ΔL₁ firewall statistic per the 2022 appendix at β = 1.

Kernel-grain validation (all four compiled projects). Each project was compiled and its ground-truth dependency graph extracted from the kernel environment (Expr.getUsedConstants over every constant's type and proof term). Textual edges are 77–92% precise against kernel truth (PFR 92%, Sphere 92%, Gauss-sphere 88%, FLT 77%) with 52–59% recall — the missing half is instance resolution, notation, and tactic-mediated uses, 68–87% of it edges into definitions rather than theorems. α and Q agree between grains within errors on every project. Tracking fidelity rises at kernel grain (PFR 73%→86%, FLT 47%→79%, Sphere 54%→66%), confirming textual levels as lower bounds — with one telling exception: Equational Theories barely moves (42%→43%), meaning its correspondence gap is real, not an extraction artifact. The ET kernel corpus is the largest: 48,505 declarations, 336,491 internal edges, α = 2.88 ± 0.07, with Magma reused 34,032 times. PFR alone makes 88,790 references into mathlib/core (≈68 per declaration); FLT 263,742; ET 272,961.

Data-quality audit (correction). A manual audit of the extracted graphs found four defects in the original textual extractor: ASCII-only identifier regexes truncated Unicode Lean names (z₁…z₆′ collapsed into one fake hub z; Greek-initial declarations dropped entirely), the Lean 4.33 public modifier was unrecognized (hiding 55% of the Math Inc corpus), string literals could produce phantom declarations, and short global names (G, f) matched same-named local variables project-wide. All were fixed and every number in this report recomputed; the qualitative findings survived unchanged, but several exponents moved (e.g. Math Inc α 1.94→2.51, ET human 2.08→2.52) and the cross-strata edge counts halved. The kernel-grain graphs, extracted from compiled binaries, were never affected — their agreement with the corrected textual numbers is itself evidence the pipeline is now sound.

Audit, second round. Further manual checks, each reading extracted data against raw source. (1) Custom commands are a textual blind spot: ET defines its 4,694 equations via a bespoke equation N := … macro, so the textual grain sees 95 declarations in Equations/ where the kernel sees 14,278 — another reason the kernel grain is authoritative for ET. (2) The certificate-dust claim survives ground truth, in stronger form: at kernel grain the machine stratum's apparent internal edges are almost all Law_X_implies_Law_Y → Equation_X_implies_Equation_Y — the same certificate auto-restated at law level (exactly one such edge per certificate pair in SimpleRewrites, Vampire, brute-force, and 4×4-table methods). Zero genuine certificate-to-certificate reuse; only the Greedy method's human-designed PartialSolution machinery shows real internal structure. And the one-way flow sharpens: 200,614 kernel edges human→machine, 37 back. (3) Compiler boilerplate is negligible: auto-generated declarations (casesOn, rec, noConfusion…) are 1.6–5.3% of kernel nodes; removing them shifts PFR kernel α from 2.46 ± 0.23 to 2.58 ± 0.27 — well within errors. (4) Blueprint extraction verified by hand: in PFR's entropy chapter, 42 hand-counted \uses dependency mentions = 42 extracted edges, multi-name \lean{} tags parse correctly, zero dangling references. (5) The AI style trajectory re-counted from raw files: AlphaProof's 2024 P2 solution contains a single have in the entire file; a sampled 2026 Nexus file has 255, of which 95% are named — consistent with the corpus-wide 97% figure.

Audit, third round — adversarial robustness of the headline claims (full numbers in results/robustness_summary.json). (1) "α ≈ 2 power law" should be read as "heavy tail": a Vuong likelihood-ratio test cannot distinguish power law from lognormal on four of the five kernel corpora (|R| < 1.96); only ET, with a 665-declaration tail, statistically favors the power law (R = +3.6). At a fixed x_min = 8 all five corpora sit at α = 2.1–2.6, and module-jackknife shows PFR's tail is partly carried by its entropy toolbox. Heavy-tailed reuse with hubs is robust; the precise exponent is not the load-bearing quantity. (2) The Wiles signature survives a grain control: contracting Lean graphs to file level (matching blueprint size) leaves α at 2.1–3.0, still below the blueprints' 3.3–4.6 — the hub deficit is a property of communication, not coarseness. (3) Tracking is not a density artifact: random pairs of the same blueprint-tagged nodes connect within 6 hops only 2–11% of the time, versus 44–86% measured — and ET's base rate equals FLT's, so its correspondence gap is real. (4) The null-model decomposition replicates on FLT (degree-keeping controls reproduce the real curve and firewall +12.5 to +13.7; modularity-destroyed controls collapse to +4.4/+5.2), and a later grid extension corrected the ER reading: the ER transition is sharp but sits at ε ≈ 0.44, outside the original grid — see "Is it actually a phase transition?" above. Seed variation moves crossover estimates by < 0.01. A CSN goodness-of-fit bootstrap adds: the power-law form is not rejected for PFR/FLT/Sphere/Gauss tails (p = 0.15–0.85) and is rejected for ET (p < 0.01, ntail = 665) — heavy-tailed and approximately power-law, with the strict form failing exactly where the data has power to test it. (5) The asymmetry result is not an anchoring artifact: adding a persistent prior field softens the pure-forward collapse (0.50 → 0.84) but the shape survives — mixed coupling still wins, forward weight still favors the final theorem. (6) The sorry-clamping contrast holds across seeds (FLT downstream −0.25 ± 0.09; Sphere −0.07 ± 0.10) though Sphere's earlier −0.007 was seed luck. (7) All 37 machine→human edges were read: they are genuine (the Sheffer development and the Tarski543 proof, which chains nine machine certificates) — so "nothing flows back" should read "0.15% of certificates have ever been reused by humans."

The parallel-task confound (audit, fourth round). An objection worth taking seriously: the magma-implication problem was chosen for parallelizability — maybe certificate dust reflects the task, not search. Two controlled tests (results/et_depth_split.json). First, human-authored implications of the same ordinary type are exactly as flat as machine ones (median construction-specific support 1 for both; even at kernel grain, 46% vs 54% cite any intermediate at all) — so the dust of the easy mass is indeed the task's doing, and the raw human-vs-machine strata comparison overstated the generator's role. Second, holding the task fixed, depth splits by method: the 34 human counterexample results carry median 33 (max 53) supporting constructions; the 1,078 machine Facts carry uniformly ≤ 2 (a stamped template); the Greedy method — a human-designed framework machine-instantiated per equation — sits between (tail to 31). The refined claim: search operated precisely on the stratum of instances where no intermediate structure is needed, and every deep instance that got solved was solved by construction. The α ≈ 2 economy is not something search lacks; it is something deep problems demand, from whoever solves them.

The missing experiment, run (audit, fifth round). The confound above demanded a corpus of search-generated proofs on mathematics not selected for parallelizability. It exists: the Mizar40 experiments (Kaliszyk & Urban) had Vampire/E re-prove 32,524 theorems of the general Mizar Mathematical Library, recording the premises each minimized ATP proof used, and the MPTP2078 benchmark encodes the human Mizar proof dependencies for 2,078 theorems on the track to Bolzano–Weierstrass. The intersection gives 1,274 theorems of ordinary mathematics — topology, analysis, set theory — each with both a human and a search-found proof (analysis/mizar_atp_compare.py, results/mizar_atp_compare.json). Results, after removing MPTP background axioms: ATP proofs are 3× leaner (5.1 vs 16.5 premises) and heavily rerouted — only 29% of the premises an ATP uses appear in the human proof's dependency set. And the reuse economy differs in the predicted direction: human premise reuse is hub-concentrated (α = 2.36 ± 0.09 on a 248-premise tail, Gini 0.740) while ATP reuse is flatter and hub-deficient (α = 3.18 ± 0.38 on a 33-premise tail, Gini 0.567); a size-matched control (human dependency lists subsampled to ATP proof sizes, 20 reps) leaves human Gini at 0.669 ± 0.002, still well above the ATP — the gap is not a proof-length artifact. Two caveats cut in opposite directions: Mizar40's premise selection was kNN-trained on human proofs, biasing the ATP toward human routes (unbiased search would diverge further), while ATP proof minimization may prune some genuinely-used context. The refined conclusion of the previous note survives its cleanest test so far: on the same general-library theorems, search finds valid but structurally different proofs — shorter, scattered, avoiding the canonical toolbox that human proofs concentrate on.

Below the naming grain (sixth round): the 2019 term-sharing analysis, rebuilt in Lean. The 2022 paper's Coq networks were hash-consed proof-term DAGs — reuse measured at subterm grain, below named declarations (code: ManipulateProofTrees). We rebuilt that algorithm over compiled Lean kernel terms (de Bruijn indices give exact α-equivalence; child order and multiplicity preserved) and ran it on all 47,940 ET proof terms (analysis/subterm_stats.lean, results/et_subterm_summary.json). The naive expectation — dust all the way down — is wrong. Machine certificates have real internal sharing: at matched term size (100–3,000 distinct subterms), machine and human proofs compress identically (10^0.87 vs 10^0.88 tree-to-DAG), and the machine's most-repeated subterm is referenced more (median max-refcount 39 vs 24). The difference is in character and in fate. Human deep constructions achieve extreme, diverse compression — the Facts counterexample towers median 10^2.0, and full_spectrum_Equation1682 packs an expanded tree of ~10^10.8 nodes into a 124,638-node DAG (one subterm used 3,101 times). Machine sharing is concentrated hammering: a heavier subterm-refcount tail (α 3.2 vs 4.1 size-matched) — the same expressions recurring down a rewrite chain. And crucially, the machine's shared subterms stay inline: they are never factored into named declarations, so their reuse dies at the term boundary. This localizes the dust result precisely: machine proofs are not structureless — they are unfactored. What search lacks is not repetition but the act of naming repeated structure into citable units, and that act is exactly what the α ≈ 2 economy, the belief dynamics, and the refutation firewalls all run on.

Interactive: the object itself

Below is the actual network the statistics in this report are computed on — the largest connected component of PFR at kernel grain: 1,106 compiled declarations (nodes, sized by how often they are reused) and 5,344 kernel-verified dependency edges. Press play to run the 2022 paper's belief model live on it: each declaration is a spin that flips toward agreement with its dependencies and dependents, with per-step error rate ε. Drag ε and watch the epistemic phase transition — above the critical point belief stays patchy and mottled; below it, conviction crystallizes across the whole proof at once.

▶ Play Reset (75% prior) Doubt all ε 0.100 color by part

mean belief – belief in PFR_conjecture' –

3Result: the signature persists — and where it doesn't

Three readings of the table. First, the 2022 universality is not a human quirk: it re-appears in every corpus built by incremental, context-bounded construction — including the 2026 AI autoformalizer. Second, it is not a machine inevitability either: saturation provers and brute-force enumeration, which find each proof independently by global search, produce a topology unlike anything in the 2022 dataset — not a longer chain, not a flatter tree, but dust plus a few enormous definitional stars. Third, the one machine method with real internal structure (MagmaEgg, greedy constructions compiled from a human-designed metatheory, mean internal out-degree 4.4) shows the divide is not human-vs-machine but constructed-vs-found.

4Result: the phase transition survives; what it rests on shifts

Every connected network still supports an EPT, and every one still has firewalls (ΔL₁ ≈ +3 to +10, within the 2022 range). But in the machine stratum the basis of certainty has changed. A Vampire certificate is an island: no sibling paths, no re-enforcement, no abductive flow from things it enables — because it enables nothing. Its truth is pinned by exactly two things: the kernel check (in the model, an external field applied node-by-node, not a network effect) and the shared definitions it instantiates. All epistemic risk therefore concentrates in the definitional hubs — which is Commelin's "ceci n'est pas une pipe" worry (are the definitions about what we think they are?) made quantitative. A single mis-stated definition in ET touches up to 13,816 dependent results; nothing in the certificate layer could detect it, since certificates never cross-check each other. The firewall structure that lets human mathematics contain error is, in the certificate layer, replaced by a monoculture root.

What structure actually produces the phenomenology (null-model controls)

The 2022 results bundle several structural properties together: heavy-tailed re-use (the α ≈ 2 degree law), modular organization (Q), and hierarchical acyclicity (proofs form a DAG). Which of these does each phenomenon actually depend on? We ran identical belief dynamics on the real PFR kernel network and on four randomized controls, each destroying some properties while preserving others (results/null_models.json). The quantities compared:

• Degree sequence — whether the control keeps each node's exact number of incoming and outgoing edges (and hence the α ≈ 2.46 power law and its hubs). "Poisson" means edges were placed uniformly at random, so the degree distribution becomes narrow and hub-free: a power-law α is simply not defined for such a graph, which is why that cell has no number.
• Q (modularity) — how strongly the graph divides into communities (0 = none; the real network's 0.61 is high).
• ε_c (transition location) — the per-step error rate at which mean belief crosses the midpoint between its ordered (≈1.0) and disordered (≈0.84) plateaus, as ε is swept from 0.4 down to 0.01. Smaller would mean the network needs more reliable inference to reach consensus.
• Max slope (transition sharpness) — the steepest change of mean belief per unit ε along that sweep. A sharp collective transition (a true EPT) has a large value; a gradual crossover has a small one.
• ΔL₁ (firewall) — the 2022 appendix statistic: at β = 1, how much more it costs the network (in log-likelihood per flipped node) to flip an entire module against the consensus than to flip the same number of randomly scattered nodes. Large positive values mean modules can sustain internal dissent cheaply but dissent cannot spread — doubt is quarantined.

The decomposition is clean, with one correction found by extending the ε grid past 0.40 (an earlier version of this section, computed on ε ≤ 0.40, misread the Erdős–Rényi control — its transition sits just outside that window). The belief curve is a degree-sequence phenomenon: every control that keeps the real degrees reproduces the real curve exactly, whether or not modularity or acyclicity survive. The Erdős–Rényi graph behaves qualitatively differently — but not by blurring the transition. It has a sharper, classic collective transition at ε ≈ 0.44: fully uncertain above it (m ≈ 0.01 at ε = 0.46), then everything orders at once. The real network instead orders in stages: at ε = 0.46, where the ER graph is still noise, the real network's hub core has already reached m = 0.32, and mean belief then climbs gradually as the sparse periphery melts in over a wide ε band. Heavy tails do not sharpen the transition — they move the onset of certainty to far higher error rates and stage the ordering, hubs first. The firewall is a modularity phenomenon: ΔL₁ sits at +11 to +12 in every graph that retains community structure and collapses to +6 in both graphs that lose it, independent of everything else. Acyclicity, notably, is needed for neither.

Is it actually a phase transition? (and is α actually the knob?)

Three sharper tests, replacing the eyeball criteria of ε_c-and-slope (results/transition_tests_*.json):

Susceptibility and hysteresis (PFR kernel). The susceptibility χ(ε) = N·Var(m) shows no interior peak in ε ∈ [0.10, 0.46] — it rises monotonically toward ε = 0.5 — so the smooth belief curve reported above is a finite-size crossover, not a critical singularity sitting at "ε_c = 0.33"; that number is a crossover midpoint and should be read as such. What is sharply present is bistability: initialized all-believing vs all-doubting, the network reaches different locked states at every tested ε up to 0.46 (hysteresis gap 0.66 even there, 1.9 at ε = 0.1). The genuinely transition-like structure in a real proof network at realistic error rates is this memory — belief and disbelief are both self-sustaining phases, and the prior decides which basin you land in. On subsampled networks of growing size the maximum slope of the belief curve grows (3.0 → 3.3 → 5.1 from N = 225 to 23k), consistent with a true singular transition emerging in the large-N limit, though subsampling distorts degree structure enough that we treat this as suggestive.

The causal arm: dialing α directly. The null models above hold the degree sequence fixed and vary everything else; the converse experiment generates synthetic directed graphs at matched size and density with the out-degree tail dialed through α = 1.8 → 4.0 (plus a Poisson control). The crossover location moves monotonically with tail weight, tracking the mean-field prediction that the critical coupling scales as ⟨k⟩/⟨k²⟩:

So α causally sets where collective belief becomes possible — heavier-tailed reuse lets certainty form at higher error rates — and the Poisson control falling on the same ⟨k²⟩/⟨k⟩ curve shows the mechanism is the degree fluctuations themselves, exactly as mean-field theory predicts. The refined headline: heavy-tailed reuse does not make the transition sharper; it moves the onset of certainty earlier (higher ε), stages the ordering hub-core-first, and makes the believing core bistable-robust across essentially the whole error range.

A coupling-asymmetry sweep on the real graph completes the picture. Here the total coupling strength is held fixed while its split varies between β_dep (forward: a claim aligns with its premises) and β_imp (backward: a claim aligns with the results that use it). Either extreme destroys collective belief. Pure-backward (β_dep = 0) leaves mean belief at 0.58. Pure-forward (β_imp = 0) collapses it to 0.50 — chance — because axioms and definitions have no premises: with nothing flowing backward, the foundations feel no field at all, randomize, and inject noise into everything built on them. Mean belief peaks near the symmetric split, while belief in the final theorem keeps rising with forward weight (reaching 1.00 at roughly β_dep:β_imp = 3:1 at ε = 0.05). The model's reading: evidence flows forward, but foundations are stabilized by what they support — belief in the axioms is partly sustained by the coherence of their consequences.

The paper's asymmetric model, taken seriously in 2D (results/asymmetric_2d.json). The 2022 paper's published curves set β_dep = β_imp "for simplicity" and introduced the asymmetric model for one mechanism: strong abduction should let disbelief in a consequence overwhelm the deductive evidence for its premises. Sweeping the full (β_dep, β_imp) plane on the PFR kernel network shows, first, that the simplification is harmless: an epistemic phase transition exists at every ratio from 1:4 to 4:1, with ε_c drifting only from 0.32 to 0.35, and the 2D plane is a wide plateau — belief organizes whenever both directions are nonzero and fails on both axes. Second, the refutation mechanism is real but gated by redundancy: clamping the network's most-reused node to false moves its premises by exactly nothing at any ratio — a premise's abductive support sums over all its consequences, and one refuted child among hundreds of believed ones is outvoted. Through fragile links (premise with only 1–2 consequences; 712 such links in PFR), doubt does propagate backward, but only once abduction dominates: mean premise drop 0.21 (max 0.79) at β_imp:β_dep = 4:1, versus 0.02 at the symmetric point. In Lakatos's terms: monsters can be barred wherever a lemma is load-bearing for many results; only claims with a single consequence are hostage to it.

5Result: three generations of AI proof style

Same three theorems (IMO 2024 P1, P2, P6), machine and human, plus the 2026 research corpus:

The 2024 system solved the problems and wrote them the way search trees look: one monolithic proof per theorem, intermediate facts bound anonymously (each have: shadowing the last — literally un-addressable), double the human case-split rate, and — as its own annotators note in the mirror repo — "the agent wastes the next 16 lines proving then discarding a lemma." Where the human formalizer of the same theorems produced 57 small named lemmas, AlphaProof produced 3 sealed blocks. Per the EPT model, such a proof cannot host a phase transition for its reader: there is one path to every claim, so doubt decays nothing and certainty comes only from the kernel.

Two years later, Nexus writes mathematics whose skeleton is indistinguishable from — indeed more articulated than — expert human Lean: 97% of claims named (with human-readable names like exists_separablyGenerated_charZero), naming density 3× the human expert, case-splitting at human rates, and claims re-used up to 17 times. The obvious deflationary explanation — imitation of human training style — is incomplete: naming density overshoots human practice substantially. The more interesting hypothesis is that addressable, modular subgoals are instrumentally necessary for any bounded-context agentic prover — the machine rediscovered lemma culture for the same reason mathematicians invented it. If so, the 2022 topology is a signature of resource-rational proving as such, and human mathematics found it first because human working memory is the tightest bound.

6Result: the correspondence problem, measured

DeDeo & Duede's tracking condition — the formal proof should realize the informal proof's inferential steps — becomes measurable with blueprints: for each blueprint edge whose endpoints carry \lean{} tags, ask whether the formal graph contains a path between the tagged declarations.

Bars: share of testable informal dependency edges realized as formal paths (≤ 6 hops, project-internal). Textual extraction under-counts, so read the gradient, not the levels — kernel-grain validation on compiled PFR raises its level from 74% to 86% (direct edges 50% → 65%), leaving the gradient intact.

The gradient tracks machine involvement. PFR — the disciplined human speedrun where the blueprint was the coordination instrument — realizes three-quarters of its informal edges formally, at a resolution ratio of 4.6 formal declarations per informal statement. ET realizes barely a third, at a ratio of 80:1: the blueprint narrates the human-facing theory while the 22M-edge machine payload lives entirely outside the narrative. The same holds for representational churn: only 213 of the human repo's 816 declaration names survive in Math Inc's AI-completed sphere-packing repo. Formal mathematics is becoming a medium in which the informal account is one projection of a much larger object it only partially tracks — the Standard View's "corresponding derivation" increasingly corresponds to nothing a human wrote.

7Common themes

8New hypotheses

9Proposed next experiments

• Dynamic EPT on blueprint git histories. Every \leanok flip is a timestamped belief-state change on a known network. Fit the Ising dynamics to the actual percolation of formalization across PFR/FLT/Sphere/Carleson; test whether progress cascades from high-out-degree nodes as the model predicts. This is the first chance to test the 2022 dynamics, not just its statics.
• Compiled-grain replication. Re-extract all networks with LeanDojo/ntp-toolkit (kernel-level premises) to close the textual-extraction gap; the mathlib-wide studies (arXiv:2604.24797; proofgraph.org, 323k declarations) provide the null model.
• Comprehension experiment. Give mathematicians matched AlphaProof-2024-style (sealed) and Nexus-2026-style (articulated) proofs of the same statements; measure error-detection, recall, and transfer. Does machine-adopted modularity actually restore understanding, or only its appearance? ProofOptimizer's 87%-compression pairs supply controlled stimuli.
• The Vampire-humanization corpus. Tao's challenge to humanize a 62-step Vampire proof (minimized to 20 steps, arXiv:2605.21200) is a paired found/constructed proof of one theorem — the ideal microscope for what "understanding-through-reuse" adds.
• Cross-layer Ising model. Extend the 2022 model with a per-node kernel field h and a definitional layer shared across proofs; derive the phase diagram in (h, β_dep, β_imp) — where does coherence-based belief become irrelevant, and what happens to global certainty when a definitional hub flips?

10Limitations

• Textual Lean extraction misses tactic-mediated and mathlib-routed edges; kernel-grain validation on compiled PFR confirms α and Q are robust (2.46 vs 2.27; 0.55 vs 0.59), textual edges are 89.5% precise with 53% recall, and tracking-fidelity levels are lower bounds (86% vs 74% for PFR). The other three projects remain textual-grain pending builds.
• ET's machine stratum proves ~22M mostly-independent implications; some structurelessness is the task's, not the method's. The Dim24/Nexus corpora control for this: same task class as human work, structure retained.
• Blueprint \uses edges are author-curated and sparser than actual dependence; the Wiles-like α may partly reflect curation. (So did Wiles's own citations — that is the point.)
• Simulation settings replicate the 2022 choices (symmetric β, prior 0.75) without sensitivity sweeps over the asymmetric regime; the abductive-paradox contours were not re-derived here.

11Sources and materials

Anchor papers: Viteri & DeDeo, Cognition 225:105120 (2022) + appendix · DeDeo, Bull. AMS 61:375 (2024) · DeDeo & Duede, arXiv:2603.13680 (2026).
Data (all public, re-extracted here): teorth/pfr · teorth/equational_theories · ImperialCollegeLondon/FLT · Sphere-Packing-Lean (human-led) · math-inc/Sphere-Packing-Lean · AlphaProof IMO 2024 raw outputs · AlphaProof Nexus results · compfiles (human IMO formalizations).
Context: ETP paper arXiv:2512.07087 · AlphaProof, Nature (2025) · Avigad, "Mathematicians in the age of AI," arXiv:2603.03684 · Tao, "Machine-Assisted Proof," Notices AMS 72(1) · Venkatesh, "Human Mathematics in the Age of Reasoning Machines" (2025) · Duede & Davey, Phil. Sci. (2025) · Leiden Declaration (2026) · mathlib network studies: arXiv:2604.24797, proofgraph.org · ProofOptimizer, arXiv:2510.15700 · Vampire-on-ETP, arXiv:2508.15856.