The Mathematical Discovery Engine — a machine that searches for new theorems
The Mathematical Discovery Engine<br>What if a new theorem<br>is just a path waiting to be found?
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 .
▶ Fly through the live graph
Explore the 3D graph<br>★ Star on GitHub
No install · runs in your browser · loads ~11 MB of real graph data
15,941 States
1,223 Techniques
26,614 Connections
∞ → finite Search Space
The Idea
Mathematics is not infinite to search. It only looks that way.
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
Search with a goal — or with no goal at all .
01 · Targeted<br>Prove a specific theorem
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.
02 · Open-Ended · By Design<br>Discover with no problem in mind
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.
The Bet<br>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 orchestra of models walking the graph .
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
Point it at a conjecture and let it search .
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.
your terminal
# 1 — get the engine<br>$ git clone https://github.com/ansumandas441/mathematical-discovery-engine<br>$ cd mathematical-discovery-engine<br>$ pip install anthropic networkx
# 2 — search for a proof (free, no API key)<br>$ python3 -m discovery_engine.discover --dry-run \<br>"Prove the Erdős primitive set conjecture"
# 3 — real models, no API key — uses your Claude Code subscription<br>$ python3 -m discovery_engine.discover --use-cli \<br>""
# …or bring an Anthropic API key for the cheapest large searches<br>$ export ANTHROPIC_API_KEY=sk-ant-...<br>$ python3 -m discovery_engine.discover --llm-orchestrate --workers 5 \<br>""
Full setup, every flag, and worker modes are documented in the README.
Read the setup guide →<br>View on GitHub
Explore the 3D graph<br>★ Star on GitHub