# Principia Labs AI for mathematical discovery - Team: Harrison (Harry) Sanders (founder) - Founded: 2025 - Invested: 2025 - Links: [Website](https://www.principialabs.org), [LinkedIn](https://www.linkedin.com/in/harry-sanders-668778201/) - Field: Reasoning and trust ## The problem: How do you build a machine that discovers new mathematics? ### How a proof gets checked A proof assistant 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. Lean is one such tool, and its community library, mathlib, 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 cap set problem, and AlphaEvolve improved lower bounds for 11 kissing numbers. ### Why it is hard **Easy to check, hard to find.** The gap between checking and finding runs deep. The P versus NP 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. **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. **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. ### 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 compressed sensing: 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. ### How they go at it **Trained from scratch.** Principia trains its own models, from scratch, to do original mathematical and scientific reasoning. **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. ### 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. ### 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. ## 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. ## Sources 1. [Proof assistant](https://en.wikipedia.org/wiki/Proof_assistant), Wikipedia 2. [Lean (proof assistant)](https://en.wikipedia.org/wiki/Lean_(proof_assistant)), Wikipedia 3. [List of mathematical discoveries by artificial intelligence](https://en.wikipedia.org/wiki/List_of_mathematical_discoveries_by_artificial_intelligence), Wikipedia 4. [P versus NP problem](https://en.wikipedia.org/wiki/P_versus_NP_problem), Wikipedia 5. [Four color theorem](https://en.wikipedia.org/wiki/Four_color_theorem), Wikipedia 6. [Kepler conjecture](https://en.wikipedia.org/wiki/Kepler_conjecture), Wikipedia 7. [AlphaEvolve](https://en.wikipedia.org/wiki/AlphaEvolve), Wikipedia 8. [Principia Labs](https://www.principialabs.org), Principia Labs 9. [The Bottleneck](https://www.principialabs.org/blog/the-bottleneck), Principia Labs 10. [Compressed sensing](https://en.wikipedia.org/wiki/Compressed_sensing), Wikipedia