Sources#

Logical Certificates Carry Neither Interest Nor Understanding#

Questions (both #oq/now, formal-math):

From Automated Conjecturing: the 6,522 survivors are statements not implied by the classical table. Is that a usable definition of mathematically interesting, or does a queue of thousands of unimplied class-conditioned inequalities relocate the triage problem from the machine to the reader?
From Logical vs Intelligible Proof: where an AI-produced result exists as both prose and a formalization, which artifact carries the understanding, and does the formalization ever change what a mathematician can do with it?

Why one page. Both ask whether a logical certificate also carries the intelligible good, in De Toffoli and Duede's sense (After Math, practitioner-opinion). On the generate side the certificate is unimpliedness by a linear program. On the prove side it is a Lean kernel check. Both questions held partial answers that rested on that opinion piece. What has been compiled since (the AutoGraphForge raw's §4.2 prose re-read for this query, Buckmaster's first-hand reading, Tao's Numberphile interview) answers both from the systems' own users rather than from the philosophers.

Short answers.

No, not a usable definition. Yes, triage relocates, and the documented reader it relocated to is the system's author. The question's disjunction is settled on its second branch, with the system's own measurement as the evidence.
The formal artifact carries certainty only. The AI prose carries understanding latently: a reader who already holds the relevant technique can recover it, even where the prose's own exposition misses it. The formalization changes one documented thing, an audit map of which prose claims are certified. What stays open needs outside evidence (below).

Labels: documented means a source states it, with its tier. Inference means this wiki's reading across sources.

1. Unimpliedness is a filter, not a definition of interest#

The certificate is narrower than the question's premise#

A correction first. The 6,522 are not all unimplied. The LP novelty test flags a candidate as a known rediscovery and excludes it "from the set of novel survivors", but the 6,522 count is taken before that split. The paper says the filter "flags 33 survivors as rediscoveries" (AutoGraphForge: Towards Automated Graph Theory Discovery §4.1, empirical). Yet the top-100 audit counts 49 "rediscoveries the novelty filter recognises" (Table 2). 49 in the top 100 cannot fit inside 33 in the whole set. Neither the paper nor Automated Conjecturing reconciles the two, so the size of the strictly unimplied set is not known exactly. The answer below does not depend on it.

What the system's own author found when he read the queue#

Documented (empirical, single-author workshop paper):

His hand read, before the count. "We manually checked the top 100 survivors by touch number. Many 'novel'-flagged survivors that we checked are, despite the heuristics and novelty filter, dominated by true-but-trivial bounds and by definitional artefacts" that "our novelty filter does not yet recognise". His example is the Sophie condition (radius ≤ k) ⇒ connected, whose hypothesis is defined only on connected graphs. This is the direct answer to the question. Statements that pass the unimpliedness test, read by a person, are mostly not interesting.
The count, after. Table 2 classifies the same 100 automatically: 49 rediscoveries, 2 subsumed, 1 decorative, and 48 "not known to us to be either trivial or false". That residue is a negative criterion, the absence of a known reason to discard. It is not a positive mark of interest.
The best of the residue. The two worked examples (ec ≤ a on bipartite graphs, a ≤ ec on regular graphs) are unimplied by the table. Each follows in a few lines from classical results that the table does not contain (Gallai, König, Pepper's α ≤ a, Petersen). The author's verdict: "Neither of these is a deep new theorem" (Automated Conjecturing, "What came out that was actually mathematics").

What this settles. Unimpliedness is relative to a 559-relation table, and the gap between "not implied by the table" and "not implied by the literature in a few lines" is where the queue's best items fall. So the certificate excludes one class of uninteresting statement, the already-tabled. It is silent on the rest: trivial, definitional, shallow-but-new. That makes it a filter, not a definition. Interest is still judged by a human reading the output, and the paper documents that the reading was done, by hand, by the author. That is the question's second branch, on the system's own record and not by analogy from an opinion piece.

The human-authored queue has the same shape#

Inference from a sibling measurement. OEIS Open's 492 human conjectures (OEIS Open Benchmark, OEIS Open: How many conjectures can language models turn into theorems?, empirical) passed volunteer editorial review. 47% sit on entries with no references, 451 of 492 sequences have zero citing works, and 37–48% of the AI-resolved ones were resolved by disproof. Human-authored queues also push triage downstream; human review filters less than a refutation battery does. So triage relocation is a property of any queue certified only negatively (not known false, not known implied). It is not peculiar to machine generation.

What the field replaced it with#

Learning to Discover Interesting Mathematics (Patel et al., empirical) is the corpus's measured attempt at a positive criterion: proof length over statement-plus-definition length. It correlates with downstream reuse on mathlib (ρ = 0.756, with the caveats on Automated Conjecturing: shared V term, zero-utility rows excluded). It shifts generation away from mathlib-contained statements (30.6% vs 91.9%), and it wins 60% of blinded four-way comparisons against no pruning, random pruning and longest-proof pruning. Inference: the existence of a better-performing positive criterion is itself evidence against unimpliedness as the definition. It does not reduce interest to a logical property either: it is a library-relative complexity ratio, and whether its picks are reused later is untested.

What the community says it lacks#

Proof Abundance (Tao, Numberphile, No More Heroes - Terence Tao Talks to Numberphile About AI, practitioner-opinion) names the shortage as questions: AIs are "depleting our pool of questions and not … replenishing them", where a solved hard problem used to produce "two new questions … as follow-ups". Inference: the replenishment he means is questions that come out of understanding a solved problem. A queue of thousands of table-unimplied inequalities is not that kind of supply, and he does not mention conjecturing systems.

What this leaves to sibling questions, all `#oq/source` on Automated Conjecturing #

whether a larger table changes the rediscovery rate;
whether "characterization or accident?" can be automated;
whether Patel's metric predicts reuse for generated statements.

None reopens this question. Each asks whether a better filter or criterion exists, and this question asked whether unimpliedness is one.

2. Which artifact carries the understanding: the 2026-10-15 answer, updated#

Which Artifact Carries the Understanding? Prose and Formal Proof as Two Objects settled most of this by splitting the question. In all five paired cases the prose and the formal proof are different objects. The formal artifact carries certainty and no documented understanding. The AI prose is the only candidate carrier, but its reception is negative or deferred. Reported understanding comes from a third, human artifact. One piece of evidence was already on Logical vs Intelligible Proof and that page did not use it, and it changes the picture of the prose.

Buckmaster read the AI prose and found the key idea (Tristan Buckmaster, The Buckmaster Interview (Navier-Stokes) - Numberphile, practitioner-opinion, auto-captions, an interested party). He says the OpenAI Navier–Stokes paper "is not … in a readable form but … the ideas can be digested". After "a couple of days" he identifies "the leap": the forced collapsing vortex is a non-solution, and the step that matters corrects it by combining convex integration with the Euler growth mechanism. He adds that this is "not what they are talking about in the introduction of their paper", and that the paper cites his convex-integration work without saying how it was used (The Navier–Stokes AI Claim).

That refines the 2026-10-15 answer in three ways:

The prose did carry the understanding, latently. This is the second first-hand report, after Bloom on Erdős #548, of an AI prose argument from which an expert extracted why it works. Buckmaster's also comes with "slop". So "reception negative or deferred" was too flat: readable is one property and recoverable is another.
The producer's own exposition did not carry it. The introduction misdescribes the key step, on Buckmaster's account. The understanding was in the argument and not in the explanation, and it took a reader to find it.
The reader who recovered it already owned the technique. Convex integration is the field Buckmaster "built my whole career on", and he had tried the combination himself "for over 10 years". Inference: what the prose transmits depends on how much of the technique the reader already has. That is why the two documented recoveries are by the curator of the problem set (Bloom) and by the one rival expert in the method (Buckmaster), and why the field-wide reception is "not yet digested".

The third-artifact pattern gets one more instance. Buckmaster is holding back "a whole bunch of results" from his own AI-assisted work and says he will spend the coming months on the "responsibility to explain our methods" instead (Proof Abundance). Tao locates what stays human in the process: AIs "can generate the final product … but … they're very bad at showing the process". So, on the documented record, understanding moves from AI prose to the field through a person, either a reader who holds the technique or an author who re-exposes it. It does not move through the formal artifact, and the AI prose cannot deliver it to a general reader on its own.

Does the formalization change what a mathematician can do? Nothing compiled since 2026-10-15 adds a case. The one documented use is still the audit map (the Navier–Stokes m+4/m+5 gap). Buckmaster's reading came from the prose, and he does not mention the Lean artifact. Tao mentions Lean only as one of the 2023 technologies that could have been adopted "while holding on to our understanding".

What stays open, and what would close it#

Nothing in the wiki can settle these; each needs evidence from outside it:

The undissolved form has no instance. No AI-produced pair has been checked lemma by lemma and found to be the same argument. Until one has, "which of two renderings carries it" has no case to apply to. Closed by a lemma-level comparison of a pair, Erdős 90 (plby/Erdos90 against the 18-page prose) being the cheapest.
No formal artifact has enabled new mathematics. Closed by a report of a mathematician extending, generalising or transferring a result from the formal artifact itself, not from the prose or a human re-exposition.
No instrument for understanding. This is the sibling #oq/source question on Logical vs Intelligible Proof. Everything above rests on testimony from three readers (Buzzard, Bloom, Buckmaster) and on the absence of other reports.

Sources drawn on#

AutoGraphForge: Towards Automated Graph Theory Discovery §4.1–4.2 and Table 2, re-read for this query: the hand-check quote, the 33/49 counts, the 48 residual, "Neither of these is a deep new theorem"
Learning to Discover Interesting Mathematics, via Automated Conjecturing
OEIS Open: How many conjectures can language models turn into theorems?, via OEIS Open Benchmark and Automated Conjecturing
After Math, via Logical vs Intelligible Proof
The Buckmaster Interview (Navier-Stokes) - Numberphile, re-read for this query (the "This is the leap" and "explain our methods" passages), with Tristan Buckmaster and The Navier–Stokes AI Claim
No More Heroes - Terence Tao Talks to Numberphile About AI, via Proof Abundance, with the Lean and process passages re-read
FrontierMath Erdős (Bloom on #548 and #1), via Which Artifact Carries the Understanding? Prose and Formal Proof as Two Objects

Logical Certificates Carry Neither Interest Nor Understanding: Unimplied Conjectures and Formal Proofs