Every great theorem in history was reached by applying a known technique to a known fact. We encoded all of it — 15,941 mathematical states, 1,223 techniques — into one graph. Now discovery isn't genius. It's search.
No install · runs in your browser · loads ~11 MB of real graph data
The Idea
You cannot search over all possible true statements — there are infinitely many. But you can search over every composition of known techniques applied to known facts. That space is vast, yet finite. And finite spaces can be searched by machines.
Galois applied symmetry reduction to the roots of polynomials. Cantor applied diagonalization to the real numbers. Wiles built a bridge from modular forms to elliptic curves. Each was a human, sometimes spending a lifetime, finding one path. This engine treats that path-finding as a search an orchestrator can run thousands of times in parallel.
Two Ways To Discover
Give it a goal. The engine searches for a chain of techniques connecting today's known axioms to that result — an automatically discovered proof. Impossible branches are pruned using known impossibility theorems (Abel–Ruffini, Gödel, Turing), so the search never wastes time on the unreachable.
Here is the wild part the architecture is built for: point it at no target at all. Take existing nodes, apply techniques no one happened to try in that combination, and ask — does this produce something new and true? A finite, searchable graph makes goalless exploration possible in principle. Wiring it up is the next frontier of this project.
If this works at scale, the bottleneck on mathematical progress was never the truths themselves — it was how long it takes a human to stumble onto the right combination.
Remove that bottleneck, and centuries of advancement could compress into a search that runs while you sleep.
The graph below is real and explorable today. Spin it, follow a chain of techniques, and judge for yourself.
How It Runs
An orchestrator model decides which techniques to try next. Worker models attempt each technique application in parallel. A pruner kills branches that known impossibility results rule out. Every solved problem adds new edges back into the graph — so the system grows a little smarter each time it succeeds. The whole structure is built by a pipeline that ingests mathematical sources and deduplicates against the existing canon.
Search For Yourself
The engine is open source and runs on your machine. Clone it, install two packages, and hand it a theorem to prove — the dry-run mode searches the graph for free. Already have Claude Code? Put real models to work with no API key at all — it bills to your existing subscription.
# 1 — get the engine $ git clone https://github.com/ansumandas441/mathematical-discovery-engine $ cd mathematical-discovery-engine $ pip install anthropic networkx # 2 — search for a proof (free, no API key) $ python3 -m discovery_engine.discover --dry-run \ "Prove the Erdős primitive set conjecture" # 3 — real models, no API key — uses your Claude Code subscription $ python3 -m discovery_engine.discover --use-cli \ "<your own conjecture here>" # …or bring an Anthropic API key for the cheapest large searches $ export ANTHROPIC_API_KEY=sk-ant-... $ python3 -m discovery_engine.discover --llm-orchestrate --workers 5 \ "<your own conjecture here>"
Full setup, every flag, and worker modes are documented in the README.