← PortfolioReasoning and trust

Principia Labs

AI for mathematical discovery

Team

Harrison (Harry) Sandersfounder

Founded

2025

Invested

2025

Links

Website · LinkedIn

The problem

How do you build a machine that discovers new mathematics?

Click anywhere on the map to pose a problem of your own, and a copy goes to it at once. Point at any problem to see how its copy is doing.One model, copied a thousand times, with each copy sent to its own open problem. Most of the problems sit where other sciences are stuck, far from the small patch mathematicians have already worked. Every guess goes through a checker: most are thrown out, and only the proofs that hold are kept.An illustration, not real data.

How a proof gets checked

A is software for writing proofs so precisely that a computer can follow every step. Checking a finished proof is far simpler than finding one, so the core checker can be tiny, in some systems under a thousand lines of code. is one such tool, and its community library, , holds over 210,000 formalised theorems.

That split between checking and finding is what makes maths a good playground for AI. A model can guess wildly, and the checker throws out anything wrong. AlphaProof used this to prove olympiad problems in Lean at the level of a silver medallist. Other systems have gone after open questions: a pre-trained language model found a new lower bound for the problem, and AlphaEvolve improved lower bounds for 11 .

Further reading Proof assistant (Wikipedia)Lean (proof assistant) (Wikipedia)List of mathematical discoveries by artificial intelligence (Wikipedia)

Why it is hard

i.
Easy to check, hard to find
The gap between checking and finding runs deep. The problem asks whether every problem with a quickly verifiable answer can also be solved quickly, and most people believe the answer is no. Think of a sudoku: checking a filled grid takes a minute, filling it takes an afternoon. Searching for a proof is the same, on a board with no edges.
ii.
Proofs nobody can read
Some important proofs are too big for people to check. The four colour theorem was the first major theorem proved with a computer, and at first not every mathematician accepted it, because nobody could check the proof by hand. Referees of the Kepler conjecture proof said they were "99% certain". Only formal versions, checked by machine, took the doubt away.
iii.
Too few mathematicians
The deeper problem is people. There are tens of thousands of professional mathematicians, and few of them know which maths problems other sciences are stuck on. Careers reward proving a theorem that refines a theorem. Five years spent on a problem from materials science rarely earns tenure.

Further reading P versus NP problem (Wikipedia)Four color theorem (Wikipedia)Kepler conjecture (Wikipedia)The Bottleneck (Principia Labs)

What Principia Labs is after

Most scientific breakthroughs start as maths problems, and Principia Labs wants models that do original mathematics, the kind that opens up a field. The model case is : if a signal has simple structure, you can rebuild it from far fewer samples than the old rule said you needed. Cardiac MRI scans that took six minutes now take less than one. The problems Principia has in mind, from the brain to high-temperature superconductors, are stuck for want of the right maths.

Further reading Principia Labs (Principia Labs)Compressed sensing (Wikipedia)The Bottleneck (Principia Labs)

How they go at it

Step 1: Trained from scratch
Principia trains its own models, from scratch, to do original mathematical and scientific reasoning.
Step 2: A thousand copies
A model can be copied a thousand times and pointed at a thousand problems at once, including ones no mathematician has looked at. The goal is a model that looks at the natural world and sees the mathematics underneath, the way a Newton or a Gauss did.

Further reading Principia Labs (Principia Labs)The Bottleneck (Principia Labs)

Still open

How much did the human do?
When AI helps produce a proof, the amount of human help can vary and often stays unclear. Prompts and pipelines frequently go undisclosed, and some results appear on company websites or social media without peer review.
Does a checked proof teach us anything?
AI agents recently produced a complete, machine-checked formalisation of Fermat's Last Theorem in Lean, about 13 million lines of code. Kevin Buzzard checked it and confirmed the result, and also noted that it "adds nothing" mathematically to Wiles's proof.
How often is it actually new?
On a set of 50 open problems, AlphaEvolve rediscovered the best known solutions 75% of the time and found better ones 20% of the time. Matching the state of the art is the common case. Beating it is still the rarer prize.

Further reading List of mathematical discoveries by artificial intelligence (Wikipedia)Lean (proof assistant) (Wikipedia)AlphaEvolve (Wikipedia)

About Principia Labs

Principia Labs has the ambition to build AIs for making new mathematical discoveries, as opposed to scoring well on tests of human virtuosity at applying existing mathematical tools (like the Putnam, etc.). The company focuses on AI systems capable of generating novel mathematical insights rather than just solving known problems.

Words used here

proof assistant: Software that helps write formal proofs and checks every step mechanically.
Lean: A proof assistant and programming language widely used to formalise mathematics.
mathlib: Lean's large community library of formalised definitions and theorems.
P versus NP: The open question of whether every problem whose answer is quick to check is also quick to solve.
cap set: A set of points in a particular grid with no three on a line; how large one can be is a long-studied puzzle.
kissing numbers: How many equal spheres can touch one central sphere without overlapping, in a given number of dimensions.
compressed sensing: Rebuilding a signal from far fewer measurements than usual, by exploiting the fact that it has simple structure.

Sources

How do you build a machine that discovers new mathematics?

Easy to check, hard to find

Proofs nobody can read

Too few mathematicians