Every major theorem in mathematics was discovered by applying a known technique to a known fact.
Euclid used proof by contradiction to show there are infinitely many primes. Euler plugged a series into a product formula to crack the Basel problem. Galois used symmetry reduction on polynomial roots. Wiles bridged modular forms and elliptic curves to close Fermat's Last Theorem. The techniques repeat — the same proof method appears across centuries and subdisciplines.
So I asked: what if you could map all of these techniques and facts into a single graph, and let a machine search for new paths through it?
That's what I built.
The core idea: proof is path-finding
Here's the insight that makes this tractable.
A mathematical proof is a chain: you start from known facts (axioms), apply a technique, get a new result, apply another technique, and eventually arrive at the theorem. That chain is a path through a directed graph.
Axiom → Technique → Intermediate state → Technique → Theorem
Instead of searching over all possible mathematical statements (infinite and hopeless), the engine searches over compositions of known techniques applied to known states — a finite, structured search space.
The knowledge graph
I started from ~100 pivotal theorems in mathematics — from Pythagoras to Perelman — tracing the discovery context, motivation, and proof ideas behind each. Then I distilled everything into a structured directed graph:
| What | Count |
|---|---|
| Axiom nodes (starting facts) | 3,791 |
| State nodes (intermediate results) | 4,994 |
| Theorem nodes (proved results) | 4,262 |
| Technique nodes (proof methods) | 873 |
| Directed edges | 23,397 |
| Technique clusters | 12 |
| Total nodes | 13,920 |
Each technique has a formal signature — inputs, process, outputs, preconditions — organized into 12 clusters like algebraic manipulation, symmetry & invariants, cross-field transfer, topology & obstruction.
The graph captures not just what is true, but how each truth was reached from earlier ones.
Walking through an example
Let's trace how the Pythagorean theorem lives in this graph.
The theorem node Pythagorean theorem has incoming edges from the technique Complete the square — that's one of the classical proof methods. Its outgoing edges feed into Compose with identity and Conjecture refinement, which means it acts as a building block for later results.
That's the power of the graph structure: every theorem is both a destination (proved by applying techniques) and a launchpad (feeding into future proofs).
The surprising connections
The most interesting part isn't the individual theorems — it's the cross-field bridges.
The technique Conserved quantity (from the symmetry & invariants cluster) connects to:
- Fermat's little theorem (number theory)
- Euler's polyhedron formula V-E+F=2 (topology)
- Eulerian path criterion (graph theory)
Three completely different areas of mathematics, one underlying proof technique. The graph makes these connections explicit.
Symmetry reduction connects Desargues's theorem in projective geometry to the Cantor-Bernstein-Schroeder theorem in set theory to Cauchy's group theorem in algebra. Same technique, different worlds.
Duality bridges Stokes's theorem (calculus), Hilbert's Nullstellensatz (algebraic geometry), and Green's theorem (vector analysis).
These cross-field transfers are exactly where novel proofs live — and the engine knows it.
How the discovery engine works
The engine reframes proof discovery as a search problem:
┌──────────────────────┐
│ ORCHESTRATOR LLM │
│ Picks techniques, │
│ evaluates results │
└──────────┬───────────┘
│
┌─────────────┼─────────────┐
│ │ │
┌──────▼──────┐ ┌───▼────────┐ ┌──▼───────────┐
│ WORKER A │ │ WORKER B │ │ WORKER C │
│ Tries │ │ Tries │ │ Tries │
│ Technique 1│ │ Technique 2│ │ Technique 3 │
└──────┬──────┘ └───┬────────┘ └──┬───────────┘
│ │ │
▼ ▼ ▼
PRUNER → removes impossible branches
│
SEARCH TREE → expands most promising node
An orchestrator LLM selects which techniques to try based on a scoring heuristic. Worker LLMs apply each technique in parallel. A pruner kills branches that violate impossibility theorems (Abel-Ruffini, Godel, Turing). The search tree grows until a path from axioms to goal is found — or the frontier is exhausted.
The scoring heuristic gives bonus points to cross-field transfers — techniques that bridge different clusters — because history shows that's where the novel proofs come from.
The 3D visualization
The entire graph is explorable in an interactive 3D viewer. Nodes glow by type, particles flow along edges showing the direction of mathematical reasoning, and you can orbit, zoom, and click to explore neighborhoods.
| Element | Meaning |
|---|---|
| Gray dots | Axioms — foundational definitions |
| Blue dots | States — intermediate results |
| Green stars | Theorems — proved results |
| Colored diamonds | Techniques — sized by connections, colored by cluster |
| Flowing particles | Direction of logical dependency |
Hover any node to see its connections light up. Double-click to explore its full neighborhood.
Try it yourself
git clone https://github.com/ansumandas441/mathematical-discovery-engine.git
cd mathematical-discovery-engine
python3 -m http.server 8765
# Open http://localhost:8765/graph_viewer_3d.html
Or run the discovery engine:
pip install anthropic networkx
python3 -m discovery_engine.discover --dry-run \
"Prove the Erdos primitive set conjecture"
ansumandas441
/
mathematical-discovery-engine
This is a mathematical discovery engine, which searches new mathematics applying techniques to existing results
Mathematical Discovery Engine (MDE)
9,466 nodes · 13,504 edges · 360 proof techniques · 2,593 theorems — explore the full graph in 3D
What This Repository Does
This repository is an attempt to encode the structure of mathematical knowledge and use it to discover new theorems automatically.
It starts from a simple observation: every major theorem in mathematics was discovered by applying known techniques to known facts. Galois used symmetry reduction on polynomial roots. Cantor used diagonalization on real numbers. Wiles used a bridge between modular forms and elliptic curves. The techniques are reusable — the same method of proof appears across centuries and subdisciplines.
This project does three things:
-
Collects the knowledge. A detailed report covering ~100 of the most consequential theorems in mathematics — from Pythagoras through Perelman — with the discovery context, motivation, thought process, and proof ideas behind each. The report spans 13 chapters organized…
What's next
The graph currently covers ~100 pivotal theorems. The obvious next steps:
- Expand coverage — there are thousands more theorems worth mapping
- Test against known proofs — can the engine rediscover proofs that humans found?
- Find genuinely new connections — cross-field bridges that no one has explored yet
- Community contributions — if you know a theorem and its proof technique, adding it to the graph is straightforward
If you work in mathematics, AI, or just find this interesting — I'd love feedback. Star the repo, open an issue, or reach out.
Built with Claude, NetworkX, and an unhealthy obsession with mathematical structure.
Top comments (0)