I built a system that discovers math proofs by treating them as graph search

Ansuman Das — Tue, 02 Jun 2026 13:50:00 +0000

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.

https://youtu.be/ypj-h_Aih5Q

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…

View on GitHub

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.

DEV Community: Ansuman Das