ByteDance Seed-Prover : Mathematicians jobs is going soon
Best AI model for solving complex maths
Every few months, there’s a new paper claiming LLMs are getting better at math. Most of those demos are just clever rewordings of high school algebra, or they rely on human-written templates hiding under the hood. This one’s different.
https://medium.com/media/ac06c1333627104e88f9810b33bda9ce/href
Seed-Prover, built by ByteDance’s Seed AI team, isn’t just throwing math at a chatbot and hoping something sticks. It’s playing in the big leagues: formal math, Lean 4, verified proofs, and competition-grade problems like the IMO and Putnam.
Seed-Prover is an LLM by ByteDance that solves hard mathematical problems by writing formal proofs in Lean, not casual explanations.
And it’s not just playing, it’s winning.
They’ve built two systems here:
- Seed-Prover — handles general math proofs in formal Lean syntax.
- Seed-Geometry — a turbocharged geometry engine because formal geometry is its own beast.
Let’s get into it.
Why Theorem Proving Isn’t Just “Doing Math”
Most LLMs can “solve” a math problem in natural language. They might say:
“Let x be the number. Then by Vieta’s theorem…”
But unless every single logical step is provable and checkable by something like the Lean compiler, it’s just storytelling.
That’s where formal verification comes in. You don’t just write “because obviously this implies that” you write Lean code that must pass the compiler.
What is Lean?
Lean is a formal proof assistant, basically a programming language and environment where you can write mathematics in a way that a computer can check every single step for correctness.
It’s not like writing math in English or LaTeX, where you can skip steps if they feel “obvious”. In Lean, you have to be explicit about every assumption, definition, and deduction, and the system will refuse your proof if something doesn’t logically follow.
Think of it as:
A compiler for math: you feed it a proof, and it either compiles (meaning it’s valid) or throws an error.
A programming language for theorems: you define objects (numbers, groups, functions), then prove things about them using commands (called tactics).
A math library: Lean ships with mathlib, a huge set of already-proved theorems you can reuse.
Training an LLM to do this is harder than it sounds because:
- Natural language is fuzzy; Lean is brutally precise.
- Even small syntax errors break the whole thing.
- Reinforcement learning (RL) needs a clear reward signal, which you can’t get if the system can’t verify the output.
Seed-Prover’s Core Ideas
1. Lemma-First Proofs
Most prior models tried to generate the whole proof top-to-bottom in one go. It’s like trying to solve a 3-hour exam question in a single breath.
Seed-Prover breaks that. It first writes lemmas, intermediate steps, small facts, reusable modules, and stores them in a lemma pool. Think of it as a scratchpad of proven facts that can be reused across different attempts or proof paths.
This shift from monolithic to modular proof generation gives three major benefits:
- You can track which lemmas (A lemma is a small proven statement used to help prove a larger result) are working and which are not.
- Lemmas can be proved, reused, or discarded independently.
- It allows merging ideas across multiple runs or proof directions.
This also means the model isn’t just solving it’s building a toolkit as it goes.
2. Iterative Proof Refinement
Seed-Prover doesn’t just try once and call it a day. It runs the generated Lean proof through the Lean compiler. If it fails, it goes back and tweaks things.
This isn’t just fixing typos. The model re-summarizes what failed, updates its belief state, and makes another attempt. It can refine the same proof 8 to 16 times in a single light inference run.
And yes, inference settings matter a lot here. They defined three:
Three Inference Modes That Define Its Scaling
1. Light Inference
- Simple iterative refinement.
- Retry the same proof multiple times (up to 8–16 times).
- Equivalent to doing Pass@64 or Pass@256 in old-school sampling metrics.
- Gets surprisingly far on problems that would otherwise need thousands of samples.
2. Medium Inference
- Think of it like inner and outer loops:
Outer loop: refining the overall proof.
Inner loop: refining individual failing lemmas using light inference.
- Great for deep, structured problems with multiple dependencies.
3. Heavy Inference
- Full search mode.
- Starts by generating thousands of conjectures about the problem.
- A conjecture is a guess: “Maybe this function is monotonic?” or “This triangle might be isosceles?”
- Each conjecture is attempted, and successful ones become lemmas.
- Lemmas are ranked by success rate, semantic relevance, and length.
- Final proof is attempted using only the best lemmas.
This mode is computationally expensive but pays off: it cracked several hard IMO problems that no other system has solved formally.
What is Seed-Geometry?
Formalizing geometry is its own monster. Diagrams are intuitive. Lean isn’t. Most systems struggle because they don’t know how to describe “draw a line perpendicular to AB through point C” without bloating into 20 lines of code.
Seed-Geometry fixes this using:
- Composite actions: instead of chaining low-level ruler-and-compass steps, it defines higher-level actions like “find the exsimilic center of two circles”.
- Custom DSL: domain-specific language made for geometry. It’s leaner (no pun intended) and maps directly to how geometric constructions work.
- C++ backend: replaces Python logic from earlier tools, leading to 100× speedups in reasoning and search.
It’s fast enough to explore 230 million unique geometry problems in a week and builds a training dataset of 38B tokens.
Oh, and it solved IMO 2025 Geometry Problem 2 in under 2 seconds.
Training Details
- Uses multi-task RL, not just fine-tuning.
- The reward signal is binary: 1 if Lean accepts the proof, 0 otherwise.
- Also includes formatting penalties to encourage writing lemmas first.
- Trained on:
Open datasets like NumiNaMath, CritiClean, Lean Workbook
A huge in-house pool of formalized IMO-style problems
The prompts aren’t just formal math. They sometimes include:
- Natural language hints
- Past failed attempts
- Summary of earlier failures
- Lemma reuse suggestions
It’s closer to how an actual human would think: “Last time I tried X, it didn’t work. What if I generalize it?”
So, How Good Is It?
Let’s talk performance, raw:
- IMO 2025: Solved 5 out of 6 problems formally. First time this has happened.
- Past IMO problems: 121/155 solved (78.1%).
- MiniF2F benchmark: 99.6% solved.
- PutnamBench (college-level math): 331/657 solved. Previous best? Just 86.
- CombiBench (combinatorics-heavy): 30% solved, still weak here.
- MiniCTX-v2 (real-world math formalization): 81.8% solved vs 44.3% from baseline
That’s a major leap.
So What’s the Catch?
None, unless you’re a human mathematician.
It doesn’t pretend to “understand” math like a human, but it doesn’t have to. What it does is:
- Systematically generate, validate, and refine reasoning steps
- Use compiler feedback as ground truth (Lean either accepts or it doesn’t)
- Avoid hallucination by chaining verifiable steps.
It’s a different way of being smart.
Final Thoughts
Seed-Prover doesn’t solve math in the usual LLM sense. It writes proofs that can be formally verified, using Lean, at the level of the IMO. That’s not a small thing.
This isn’t about showing off reasoning tricks or clever hacks. It’s about building a structured, verifiable, modular approach to mathematical problem solving. The kind humans take years to learn and still mess up.
If they keep scaling this system more problems, better inference loops, tighter integration with formal libraries it’s not crazy to imagine that some research-level math problems might eventually fall.
And maybe that’s what formal AI math looks like in the end: relentless correctness over poetic elegance.
ByteDance Seed-Prover : Mathematicians jobs is going soon was originally published in Data Science in Your Pocket on Medium, where people are continuing the conversation by highlighting and responding to this story.
