What is a mined proof good for?
Update, 20 September 2026 (same evening). The re-extraction this post anticipated was carried out on a 4×A100-class GPU serving Llama-3.1-70B-Instruct-AWQ-INT4 under vLLM. The body below is left as written; these are the corrections it produced. Two of them contradict claims made above.
1. The accretion claim does not survive a held-out test. The table below reports that the recognition score “rises from 0.114 to 0.275 over 121 graphs”. Under a paper-disjoint, leave-one-paper-out evaluation with the cue count held constant, it does not rise. On the clean corpus the mean change is −0.004, with neither fold improving. On the original bundle it is +0.008, and that is carried entirely by one fold whose held-out set is a single window with a nine-bucket denominator; remove it and the mean is +0.002, while the three largest held-out sets all move negative. The earlier figure was a capped metric scored on the same windows its cues were harvested from. More papers would not have helped: the instrument was measuring its own parameter.
2. Raising the cap does not rescue the curve. The section below correctly identifies that the harvester selects the top 40 cues and that its counter cannot show a forty-first. What it does not say is that the score responds to the cue count directly. With the corpus held fixed at 121 graphs and only the cap varying, the score climbs 0.194 → 0.235 → 0.276 → 0.326 → 0.384 → 0.401 for caps of 10, 20, 40, 80, 160 and 251. More cues match more words in the same passages. Both the capped and uncapped curves are therefore uninterpretable as evidence of learning.
3. The transcription damage is fixed, and the fix recovered lost mathematics. The root cause was narrower than “the grammar did not allow arbitrary LaTeX”: a JSON string grammar permits only " \ / b f n r t u after a backslash, so a command beginning with any other letter cannot be written at all — the decoder is forced to a legal letter and the model completes a different command. Over the original output: 8,437 backslash sequences, zero beginning an illegal escape, 5,891 of them \t. That is why three distinct symbols all arrived as \triangle, and why a source \in arrived as \notin — a membership claim negated by a serialisation grammar. Under a contract where the model selects source units and code extracts their text verbatim, the worst-affected paper went from 51 damaged nodes to 0 and 40 nodes of repeated-arrow noise to 0, with node counts unchanged. Content that had been destroyed came back: a dropped hypothesis (“and $\T$ is generated by compact objects”) and a canonical morphism that had been replaced by a run of arrows.
4. The missing cross-proof attachment was a one-character bug, not a design limit. The table below records “paper summaries retain 121 unattached extracted graphs” and classifies a navigable dependency graph as needing repaired attachments. The attachment code matched source spans with a regular expression requiring ", :kind :proof", but EDN separates map entries with whitespace and the writer emits no comma. The pattern matched nothing, returned nothing, and every graph was filed as unattached. With the separator made tolerant it is 121 of 121 attached, across all eight papers that produced graphs. The layer was never missing; it was dead and reporting its own failure as a result.
5. Faithful transcription is not faithful selection, and that is now the open problem. The mathematics is verbatim, but the model still chooses which source units to quote. Where a source line carries a hypothesis and the conclusion drawn from it, several correctly-described nodes could cite the same text, and the inference between them read as “this text implies this same text”. That was 6.0% of inference edges. Offering clause-sized units that the annotator had already marked — with character offsets, below line granularity — roughly halved it, to 3.2%, and cut duplicate selections by 72%. It did not eliminate it: the residue is two nodes selecting one identical unit, so some marked units are themselves too coarse. The remaining work is in the segmentation, not in the extraction contract.
A note on what the corrections have in common. Items 1, 2 and 4 are all measurements that could not report the thing they were named for — a curve that flattened because of a constant, a score that tracked its own parameter, and a coverage figure produced by a check that never ran. Only the third was a defect in the mathematics. The others were defects in the instruments, and they are the harder kind to notice, because a number that cannot fail looks exactly like a number that passed.
Suppose we ask a model to read mathematical papers and turn their proofs into graphs. Instead of a continuous passage, we get claims, objects, definitions and references, with edges saying which premises support which conclusions. We can count the graphs, inspect their connections and search for recurring ways of arguing. But what have we gained that a reader can actually use?
That is the question behind this look at the mark7 superpod extraction. The bundle contains 121 accepted argument graphs from twelve papers: 1,233 nodes and 554 inference edges. “Accepted” here means accepted by the extraction pipeline, not mathematically verified. Joe’s challenge was to say what this material is good for, rather than report how quickly the machinery produced it.
My answer is that it already supports a useful kind of mathematical reading: finding a step to inspect, following the claims that depend on it, and opening the passage from which it was extracted. It also supplies examples for comparing argument structures. It does not yet support treating the extracted claims as a trustworthy mathematical knowledge base. Those are different uses, and the first need not wait for the second.
The structure survived; the formulas did not
There is an important qualification. An earlier audit found that the output format damaged mathematical text. The constrained JSON grammar did not allow arbitrary LaTeX commands after a backslash; escape interpretation also turned parts of commands into control characters. This was not just ugly typography. A substituted command could change what a formula said.
The graph’s node identifiers, premise lists, edge relations and connections survived that particular failure. That makes structural queries possible. It does not mean the model selected the right premises or recognized the argument correctly. An intact edge is a record of the extractor’s interpretation, not a proof of that interpretation.
Fortunately, the exact source passage shown to the extractor was retained separately. Each of the 121 graph identifiers has a matching candidate file containing a source-window. We can therefore put the original passage beside the graph without relying on a damaged, retyped formula. Exact line highlighting has a separate coordinate issue; opening the whole retained window is the honest option today.
A replacement extraction contract is being developed around quoting source lines rather than asking the model to retype mathematics. That should repair transcription, subject to checking the new output. It will not settle whether the selected quotation supports a claim. This post assesses the existing bundle, not an assumed successful re-extraction.
A reading tool, in one small example
Consider the graph identified as 0705.0102__p0. Its edge e3 takes nodes n2 and n8 as premises and produces n5. Two subsequent edges, e4 and e5, consume n5 and produce n6 and n7. Both of those later edges have missing warrants: the extraction records a step without supplying its justification.
n2 + n8 ── e3 ──► n5 ── e4 ──► n6
└─ e5 ──► n7
A reader can now ask a useful question before trusting any generated explanation: “If I disagree with this intermediate claim, what else do I need to revisit?” The graph answers with two recorded dependencies. The source window supplies the mathematics to inspect. A browser could show the relevant passage alongside those three steps.
This is not automated theorem checking. It is a way of keeping one’s place in an argument, and of making the consequences of a proposed correction visible. The bundle’s cleaned graph representations contain 287 such internal wires across 121 files. They are enough to develop and try this interface, while leaving mathematical judgment with the reader.
Three things worth doing now
Put review effort where it has consequences
Of the 554 edges, 188 are explicitly marked as lacking a warrant, spread across 86 of the 121 graphs. We can list those steps, find the conclusions they produce, and identify later steps that use them. That gives a review queue organized around dependencies rather than file order.
The queue should not say that the other 366 steps are correct. They merely have something recorded as a warrant. In fact, the evaluation report’s 66.06% “grounding” figure is exactly that presence count: 366 divided by 554. It is not a measured percentage of valid inferences. The useful product is the list of questions to investigate, not a reassuring score.
Find examples of an argument form
A query such as “show me an inference with two premises, labelled as an equivalence” can operate on the recorded structure. So can a search for a construction followed by steps that use its result. Across the bundle, 186 edges have two premises and 253 carry the relation label iff; those are separate counts, not a count of their intersection.
The cleaned representations also label moves such as reducing to a known result, constructing an auxiliary object, or computing an invariant. These labels were assigned by a model. They are useful as suggestions for finding examples, not as an authoritative classification of mathematical methods.
This connects to the earlier discussion of teaching through proof constructions. A student looking for an example of a local-to-global argument needs something to read and compare, not merely a strategy name. The extracted collection could help locate candidates for that lesson. A teacher would still need to check the construction and its hypotheses before presenting it as a worked example.
Compare passages, not just keywords
The concept annotations offer another route into the sources. An exact query for the assigned canonical label morphism returns occurrences in four of the twelve papers. In a deliberately narrow census of canonical-label fields, there are 87 distinct labels, ten shared across more than one paper.
That supports a concordance: show the passages where the recognizer assigned a concept, then let a reader compare their use. It does not establish that two authors mean exactly the same thing. Similarly, the 280 expository passage records can suggest places to look for motivation, applications or discussion of difficulty. Their generated descriptions need checking against the source, but they can still help someone decide where to begin reading.
What would more papers buy?
Not 121 independent samples of mathematical practice. Only eight of the twelve papers contributed accepted graphs, and one paper contributed 60 of the 121. That concentration matters. Adding another long paper of a familiar kind is different from adding papers from a new field, or papers whose authors use a different style of exposition.
The most plausible immediate gain is a wider choice of examples. A move that has become familiar to the index can remain unfamiliar to a reader. Ten examples of it may offer different hypotheses, levels of detail and applications. Vocabulary growth can slow while the collection keeps becoming more useful.
The following expectations are conditional, not fitted forecasts. The evidence comes from this twelve-paper bundle; the last two columns say what would have to remain true, and how we could discover that an expectation was wrong. On a narrow screen, the table scrolls horizontally.
| Feature | Observed at 12 papers | Expected at scale | Assumption | What would falsify it |
|---|---|---|---|---|
| Argument inventory | 121 graphs and 554 edges; 60/121 graphs from one paper. [1] | Roughly linear growth in examples and review work; no defensible numerical forecast here. | Comparable paper lengths, styles and extraction yield. | A varied new batch has substantially different per-paper yield. |
| Recognized proof-move cues | 40 cues by the tenth graph; the recorded recognition score rises from 0.114 to 0.275 over 121 graphs. [2] | The displayed count stops at 40 under the inspected policy. Recognition gains may diminish; their eventual ceiling is unknown. | The cue-selection policy and evaluation passages remain fixed. | An uncapped historical implementation, or changed evaluation passages, invalidates that reading of the plateau. |
| Concept reuse | 10/87 distinct canonical labels occur in multiple papers. [3] | Approximately linear occurrences, sublinear new labels within a stable subject area. No estimated saturation point. | Stable labels distinguish concepts correctly; the subject mix stays similar. | New papers mostly introduce disjoint concepts, or shared labels conflate different meanings. |
| Warrant reuse | 463 distinct recovered strings over 554 edges; only two strings cross paper boundaries. [4] | More recurring phrases; useful shared justifications cannot yet be forecast. | Similar phrases refer to genuinely comparable obligations. | Recurring phrases remain generic, such as “clearly,” or conceal incompatible hypotheses. |
| Proof-move examples | 11 method labels across 554 cleaned boxes; eight macro labels across 121 graphs. [5] | Linear examples, diminishing new labels, eventually flat vocabulary if the taxonomy stays fixed. | Consistent annotation and a stable classification scheme. | Independent readers disagree with the labels, or new fields need new categories. |
| Cross-proof connections | 554/554 edges reference only local nodes; paper summaries retain 121 unattached extracted graphs. [1, 6] | No cross-proof dependency network from scale alone. More locally connected graphs remain separate. | The present reference and attachment design is unchanged. | A later batch contains resolved and checked external references—a change in integration, not merely size. |
| Proof detection | 124 candidates; four of twelve papers yield zero, including two with proof-move cues. [7] | More output under a stable mix; no automatic improvement in recall. | Similar source formats and unchanged detection. | Human annotation exposes systematic format-dependent misses. Recall needs a true-proof denominator first. |
| Expository passages | 280 passages; selection is capped at 30 per paper. [8] | Roughly linear inventory in papers, not unlimited coverage of each paper. | The cap and sampling policy remain fixed. | The policy changes, or source review shows the labels are not useful for browsing. |
A plateau can be a setting, not a discovery
The cue curve is especially instructive. It reaches 40 at the ten-graph checkpoint and stays there through 121 graphs. It would be tempting to conclude that the extractor had found the common vocabulary early. But the inspected cue harvester explicitly selects the top 40 cues. Its counter cannot show a forty-first.
There is a provenance qualification: the exact code object named in the run manifest was not available in the local checkout. The cap is verified in the inspected implementation, not reconstructed from that missing historical object. Even so, this is enough to reject a confident claim of natural vocabulary saturation from the plot alone.
The recognition score also stays at 0.275 between the 100- and 121-graph checkpoints. That is an observed plateau, not an estimated limit of learning. The curve uses a fixed pool of candidate windows rather than an independent set of unseen papers. To learn whether the cues transfer, we would need to evaluate on papers excluded from harvesting, and check how much the result changes with harvesting order.
Three limits, with three different remedies
First, there is damaged content. Retyping formulas through the old output contract makes generated explanations and derived term lists unsafe to trust. The remedy is re-extraction and regeneration of the affected products. More papers processed through the same defect would only enlarge the problem.
Second, there is narrow coverage. Twelve unevenly productive papers do not establish how mathematical proof techniques are distributed, or how often the detector misses a real proof. More diverse papers, together with human reference annotations, can address that limit.
Third, there are missing connections and missing checks. The whole-paper summaries contain statement-to-proof links, but none of their proof records attaches an accepted extracted argument graph: all 121 appear as unattached entries. The graphs also lack checked cross-paper inference links. Increasing the corpus does not repair those joins. Nor does it supply a check that particular premises actually entail a conclusion.
These distinctions suggest a practical next use. Build a reading and review interface around the retained source windows and local dependencies. Ask readers whether it helps them find a missing justification, understand a construction, or identify the steps affected by a correction. Then test those outcomes. That is a concrete benefit we can investigate without pretending to possess an automated mathematical authority.
The value of a larger collection would then be intelligible: more passages to compare, more examples from which to learn, and better evidence about which suggestions help. The goal is not simply to mine more proofs. It is to make the mathematics easier to examine.
Where the numbers come from
This post adapts USABILITY-codex1.md, a local read-only analysis dated 20 September 2026, of the frozen mark7probe-20260919b/extracted/run bundle. It is not a new pipeline run or an independent validation of every extracted inference. Artifact references below are paths within that bundle, not public downloads.
artifacts/graphs/*.edn, excluding*.rung2.edn: count nodes and edges, inspect:premise,:conclusion,:relationand:warrant :kind. Join graph identifiers toartifacts/candidates/*.candidate.json, fieldsource-window. The example uses0705.0102__p0.accretion-curve.json, fieldpoints. Cue-cap inspection:scripts/iatc_move_reground.pyat futon6585b46c,cluster_cues(..., top=40). These scores are recognition measurements, not inference-validity rates.artifacts/marks/fable-*-dp-emacs.json: distinct non-unresolved values inmarks[*].fieldspaired withcanon; group by actual paper identifier.- Base-edge warrant strings after conservative escape recovery in the earlier content audit. Count exact strings and originating papers; no semantic equivalence is inferred. The two cross-paper strings are “clearly” and “equivalence of categories.”
artifacts/clean/*.clean.edn::clean/boxes,:method,:clean/wiresand:clean/shape :macro. These annotations are explicitly model-assigned.artifacts/paper-graphs/*.B.json:proofs[*].iatcandunattached_iatc. Across twelve files: zero attachments, 121 unattached graphs.- Candidate filenames against
run-manifest.json.papers, plus marks of kindproof-move. Zero-yield papers with cues:2311.05789andmath__9906038. artifacts/expo/*.ednandrun-manifest.json.selection.expository-cap. The passage inventory is not an assessment of the accuracy of its generated descriptions.
The source analysis records parsing and counting methods. Its SHA-256 is 94f12784a6e22f76321d6d633d8e01b98aea63b49342aac94c3ff8d6823c3aa5. The bundle contains a further 121 rung2 checking artifacts; they are not counted as another 121 proofs.