An agent-driven research library for open mathematical conjectures. It records attempted approaches — including, especially, the failed ones — so that the next attempt, by anyone's agent, starts from what is actually known rather than from scratch.

Built by an autonomous Claude loop over July 2026, adversarially verified, and published so others can point their own agents at it.

Readable version: joe975.github.io/math-lab — each conjecture explained in plain terms, what a breakthrough would and would not mean, and a report on every approach tried.

7 problems, 11 attempt records, ~20 reusable tools, 12 verified results and 4 recorded dead ends. The headline standing, in the lab's own vocabulary:

No conjecture here is solved, and none is close to solved. That is the expected outcome and the honest framing: the deliverables are the approach library, the tooling, and progress on the smaller open problems.

Point an agent at AGENTS.md. It picks one of two modes:

• blind — scripts/blind.sh <problem> ../work gives it the statement, the verification harness and the rules, and physically none of our prior art. Its result is independent evidence.
• informed — a normal clone. It reads prior-art.json to see which mechanism families are already spent, then attacks a labeled gap.

The cut between those two is machine-readable (tiers.json) and enforced in CI: if a finding of ours leaks into a file a blind agent can see, the build fails. Tier-0 files contain published background only.

Every attempt records which mode produced it. That makes the library a dataset on a question nobody has clean data for: does prior knowledge help, or does it anchor? If blind agents keep rediscovering our dead ends, the prior art is load-bearing. If they keep finding things we were steered away from, our framing is a local optimum. Either answer is worth having.

An hourly autonomous cycle: read the ledger and standing guidance, pick 2–4 attack lines from the queue, fan out parallel subagents, then adversarially verify everything claimed — independent skeptic agents whose default stance is refute, with computational claims re-run by a separate implementation. Only survivors enter the ledger as results.

That process has visibly caught its own errors, which is the main reason to trust the rest. Attempt 004 is a skeptic pass that found a false proof claim and a wrong headline constant in attempt 003, and both records are kept, uncorrected in place, with the correction recorded against them.

No automated loop is running right now, but the library is open and meant to be extended — by this lab's own cycles or by anyone else's agents. Nothing is half-finished: every line pursued is written up, and STATUS.md carries a queue of concrete starting points. docs/CYCLE.md is the operational prompt for running a cycle, so the loop can be picked up rather than reconstructed.

Start at AGENTS.md if you are (or are directing) an agent. Otherwise:

• STATUS.md — live state, per-problem status, queue, insights, dead ends.
• problems/<name>/PROBLEM.md — statement and published background (tier 0).
• problems/<name>/prior-art.json — one line per attempt with mechanism tags; read this before the prose.
• problems/<name>/PRIOR-ART.md — narrative summary of what we tried.
• problems/<name>/attempts/NNN-*.md — the full records. Long; read selectively.
• harness/ — shared verifiers and generators (tier 0).
• problems/<name>/explore/ — route-specific tooling (tier 1).

These are what the repo is for; CONTRIBUTING.md has the full version.

• Nothing becomes a "result" without surviving adversarial verification.
• Dead ends are first-class output. Every abandoned approach gets a record explaining why, so nobody re-treads it blindly.
• Computational evidence is labelled EVIDENCE, never proof. Say the range.
• Speculation is labelled SPECULATION inline, at every unproven step.
• Machine-transcribed sources are marked as such, because transcription errors are real.

Python tools need only the standard library unless their docstring says otherwise. The C kernels are built from source:

cc -O2 -o harness/erdos-gyarfas/cycle_filter   harness/erdos-gyarfas/cycle_filter.c
cc -O2 -fopenmp -o harness/erdos-straus/es_fcount harness/erdos-straus/es_fcount.c
cc -O2 -o harness/graceful-trees/graceful_core harness/graceful-trees/graceful_core.c

Graph generation uses nauty's geng (Ubuntu: apt install nauty). Harness runners write to $MATHLAB_OUT (default ./out).

Tests:

pip install pytest && python -m pytest tests/ -q

Every attempt record was written by an AI agent and adversarially reviewed by other AI agents. No claim here has been peer-reviewed by a human mathematician. Treat VERIFIED as "two independent machine implementations agree", which is a real but limited guarantee — and treat anything labelled SPECULATION as exactly that.

MIT — everything: tools, prose, records and data. Use it, fork it, adapt it, sell it, no permission needed.

A citation is appreciated but not required beyond MIT's notice condition; metadata is in CITATION.cff. If you reuse a result, please carry the provenance caveat above with it — that request is a norm, not a licence term.

Nothing here reproduces anyone else's copyrighted expression. Where the records engage with published papers (Gilmer, Sawin, Chase–Lovett, Liu and others), they restate constructions and theorem statements in this lab's own notation with citations — mathematical content, not quoted text. Attempt 003 flags that some details of Liu's construction came from a machine transcription rather than the PDF, marked [L], and attempt 004 records that caveat as a residual risk.

Enumeration data under problems/*/data/ is factual output from searches run here. Graph generation used nauty's geng, which is not bundled — install it separately.