Taggart Tufte, July–August 2026. Something I wanted to try, and what I got
out of it. Every claim below points at a reproducible bundle under verify/
or a dated entry in CAMPAIGN_LOG.md; the working-level detail lives in
GUIDE.md.
A two-week experiment in machine-assisted mathematics with a trust protocol. A language model (Claude) orchestrated classical certificate-producing tools — automated theorem provers (Vampire, E, Twee, Prover9), the finite model finder Mace4, the SAT solver kissat, and GAP — against open problems on stale lists in quasigroup, loop, and semigroup theory, running unsupervised overnight on one desktop CPU. No cloud, no paid compute.
I did not expect to find anything. The project's own guide, written at the start, predicted "a well-documented sweep, not a famous kill." The design rule written down before any result existed — model prose is never evidence; only certificates count — turned out to matter more than the tools.
- Under-saturated. The people pointing language models at open problems are mostly camped on erdosproblems.com — combinatorics and number theory, with a legible database and a public "solved" tracker. Abstract algebra's problem lists (the Kourovka Notebook, Belousov's quasigroup problems, the loop-theory lists, Lyapin's semigroup notebook) are PDFs and scattered web pages. Far fewer people are running anything at them.
- ATP-friendly. Equational algebra is the historical hunting ground of automated deduction — the Robbins conjecture, Belousov's F-quasigroup problem, and the AIM loops program all fell to automated provers. Problems here state as first-order or equational sentences that tools attack directly.
- Verification mostly disappears. The deliverables are machine-checkable certificates — finite models, proof objects, DRAT proofs — not prose proofs.
- The ETP lesson. Tao's Equational Theories Project found classical provers far cheaper than LLMs and able to handle almost everything the LLMs could. So the model's job here is orchestration — harvesting, triaging, encoding, interpreting, literature-checking — not proving.
Modern provers (Vampire, E, Twee at 2026 strength) are dramatically stronger than the 2005–2015 tools that last swept these lists, and nobody had systematically re-swept the stale lists with current tools plus LLM-scale encoding and triage. That re-sweep was the campaign.
The strategy was certificate-first: a result is a precise statement plus a
machine-checkable certificate plus an independent check plus a novelty check.
Anything less — including a beautiful prose proof from a language model — is a
lead, not a result, and gets logged as one. The full protocol is in
VERIFICATION.md.
Attempt, then classify. Difficulty is measured by cheap probe runs, never predicted by judgment — a 60-second run is ground truth, a prediction is not.
- Harvest problem lists and gate on encodability (can it be stated in first-order or equational logic over one structure? is there a finite-counterexample face?). Discards are logged with reasons.
- Encode by family — one axiom template and one sanity battery per axiom family (a known theorem must prove, a known non-theorem must not), then instantiate per problem. No new encoding runs live until its battery passes.
- Calibrate on problems from the same lists that older provers already solved, to validate encodings end to end and measure the actual edge.
- Probe ladder: every target gets Vampire, Twee, E, and Mace4 for 60 seconds; survivors escalate to 10 minutes, then overnight boxes.
- Verify any hit through the protocol — independent re-implementation, literature sweep, and a private is-this-known email to an expert before any public claim.
| Result | What was shown | Certificate | Novelty verdict |
|---|---|---|---|
| Recursively 1-differentiable quasigroups, orders 14 and 18 (Couselo–González–Markov–Nechaev 1998; equivalently recursive [4,2,3] MDS codes) | Both remaining open orders exist. Order 14 has a closed form checkable by hand. | 7 multiplication tables, each verified by three independent implementations (SAT encoding, Python, GAP). verify/W20-q14-q18/ |
Every source still listed 14 and 18 open as of July 2026 (order 42 fell in 2008, order 26 in April 2026). The author of the order-26 paper was asked by email on 2026-07-28; no reply as of 2026-08-21. |
| Power-semigroup determinism (Lyapin's Notebook 5.1, finite case) | P(S) ≅ P(T) ⇒ S ≅ T for all semigroups of order ≤ 6 (218 + 1,915 + 28,634 isomorphism classes, zero collisions). | nauty canonical certificates; dual GAP/Python implementation. verify/lyapin-5.1/ |
Apparent first: the finite case is called open in three 2024–2026 papers and no published theorem covers the non-completely-regular pairs. |
| Commutative semigroups with exactly 4 endomorphisms (Lyapin 3.12, finite face) | Exactly 7, all of order ≤ 4. | Dual-implementation census, zero mismatches. verify/lyapin-3.12/ |
Partially known: finiteness is Kublanovsky 1983, the order bound is Borisov 2010; the explicit census was not located anywhere. |
| Further Lyapin items (3.2/3.4, 5.3, finite faces) | Every commutative semigroup of order ≤ 7 has at least as many endomorphisms as elements (so a 3.2 counterexample needs order ≥ 8); every commutative semigroup of order ≤ 4 embeds in the power semigroup of some commutative semigroup. | Sweeps + checker-verified witnesses, encodings/session6/. |
Unchecked against the literature; a question-framed email to the Notebook's editors was drafted and not sent. |
| QPTP JKVxx_2 (loop-theory benchmark, unsolved by all six provers in the 2008/2010 studies) | Proved by Twee in 23 s, confirmed by Vampire in 206 s at 8 GB. | Proof objects. verify/JKVxx_2/ |
Benchmark result, not new mathematics — the theorem was published. The library's co-author later confirmed it was itself originally found with Prover9, so the loop closes: ATP-born theorem, ATP-reproved 18 years on. |
| QPTP JKVxx_3 | Mis-encoded as distributed: the defining equation of f is missing, so the stated goal is false (order-2 countermodel) and trivial once restored. It survived 18 years as "unsolved" because the original studies ran no model finder. |
Hand-checkable countermodel + script. | Reported to the maintainer; erratum acknowledged, August 2026 (note to be posted on the QPTP site). |
| Alternative loops without two-sided inverses (W23) | None of order ≤ 16. | 12 Mace4 exhaustion certificates. verify/W23/ |
Subsumed: the proposer had swept to order ≤ 185 in an unpublished 2004/05 note. Kept as a reproducibility artifact and as the example of the novelty check working after the fact. |
| Alt ∧ LIP ⇒ IP (the one cell W. D. Smith's 2005 table left unresolved) | No counterexample of order ≤ 13; none with cyclic symmetry ≤ 30; no proof at 2026 prover strength in 4 h / 12 GB boxes. | Exhaustion certificates + search logs. | First explicit bound for that cell. Still open. |
| QPTP KKPxx_2a/2b | Traced to a lemma in Kinyon–Phillips (2005). The "twin" one-sided-inverse statements are trivial theorems; the conjectures themselves are equivalent to injectivity of a left translation — automatic in any finite model, so any countermodel is necessarily infinite. | Proofs, a refuting model for one reading, an implication lattice of 13 related identities. | Still open; the reduction is the contribution. |
Plus three method studies on guiding provers: (1) hint mining from target-specific subgoal decompositions turns a theorem all four untuned provers fail into a 640 s Prover9 proof, with an ablation showing hints save memory, not just time, and a pollution experiment showing irrelevant hints are free; (2) lemma injection helps Vampire/E and kills Prover9 — feed each prover its own kind of guidance; (3) a preregistered test of novelty-search lemma proposal (Stanley–Lehman style, over finite-model "truth vector" descriptors) did not beat goal-similarity selection — a banked negative. The recurring obstacle across all three was an empty difficulty band: candidate lemmas were either instant or hopeless, with nothing informative in between.
The point of the project was less the theorems than the scaffolding that decides when to disbelieve the machine. Over nine sessions it caught:
- Two bogus 0.00-second "proofs" from the same encoding trap (an identifier the prover silently treated as a variable). Caught by a standing rule that a suspiciously easy proof is a red flag, and by a model-zoo dry run that found zero models where a known one had to exist.
- Three verdict-parsing bugs in my own runners that would have recorded failed searches as hits or memory deaths as "unknown." Caught by checking raw output against summaries — the summary is not the evidence.
- A mislabelled axiom (left Bol staged as Moufang) that produced a beautiful, wrong model at order 8 — caught by a rediscovery ladder built in specifically as a lie detector.
- Two "results" that were technically valid and mathematically worthless (all generators collapsed to the identity). Retired, not counted.
- My own overstatement that a control run had "rediscovered" a published object; a stronger check showed mine was weaker. Corrected before anything was sent.
- Prior art found after banking a result (W23). The novelty stage exists precisely for this; the relabel is left visible.
- A hardware "fact" that was a setting. Four sessions were optimized inside a 23 GB memory ceiling that turned out to be WSL's default, not the machine's.
The mathematics is niche. The best result here — two orders of a 1998 conjecture closed, completing it for every order where it is not provably false — is the kind of thing that appears as a short preprint and makes no ripple; its direct comparable (order 26, April 2026) made none. The cases fell in seconds once a domain expert's stated intuition (cyclic symmetry) was encoded as a constraint, after 24 hours of unconstrained search found nothing. That contrast, not the tables, is what I think transfers: the hard part of automated research is not getting the machine to search, it is building the rules that tell you when to disbelieve it — and writing those rules down before you have a stake in the answer.
The pre-registered expectation was "a well-documented sweep, not a famous kill." It landed slightly above that. I'm leaving it here.
Alt ∧ LIP ⇒ IP (bound ≤ 13; attack the infinite side); KKPxx_2a/2b (needs an
infinite Bol magma or a first-order proof nobody has found); Lyapin 5.1 at
order 7 (≈ 10⁶ classes — the canonical-labelling pipeline in
encodings/session7/ scales); a general construction behind the order-14/18
witnesses (four hypotheses falsified in notes/w20-structure.md).
GUIDE.md — the detailed internal guide (full methodology, model allocation,
budget, mid-campaign status). VERIFICATION.md — the protocol. verify/ —
result bundles, each with a README, SHA256 sums, and a rerun.sh.
CAMPAIGN_LOG.md — session-by-session record, newest first, including
everything that went wrong. TOOLS.md — the stack and how to invoke it.
encodings/ — statements and encodings per target.