LLM Math Roaster

For Episode 22 (November 21, 2025), Jordan vibe coded the LLM Math Roaster with our guest's company, Axiom Math, in mind. It sends a math problem to four models, asks each for a formal proof in Lean 4, has ChatGPT judge the results, and ranks them on a leaderboard. He called it "productionalized" and gave it history, custom problems and an API. He didn't say how long it took.

Why we built it

On our first call with Axiom founder and CEO Carina, we talked about vibe-coded apps that could be fun for math and useful to her team. Axiom is building an AI mathematician that writes proofs in Lean, so a tool that pits models against each other on Lean proofs was a natural fit. Jordan was upfront: "I'm okay at math but I'm certainly not your level."

The stack

• Gemini 2.5 Pro, GPT-5, Claude Sonnet 4.5 and Grok 4 Fast: the four contestants.
• ChatGPT: the judge that scores every answer.
• Lean 4: the proof language each model must write in.

Jordan wanted Grok 4.1, Gemini 3 and GPT-5.1 too, but they had just launched and he didn't have API access in time. The episode didn't name the coding tool he used.

How we built it, step by step

1. Collect a problem set. About 10 problems of different difficulty. Even the Pythagorean theorem felt too hard as a sanity check, so the easiest is 2 + 2 = 4.
2. Fan each problem out to four models with a request for a Lean 4 proof, and show response times.
3. Compare side by side, then have ChatGPT evaluate every response and score it.
4. Keep score. A leaderboard, a history of past runs, custom problem submission, and light and dark mode.
5. Add an API. Axiom's team can generate their own key and submit problems in the background.

So I chose ChatGPT. So ChatGPT will then evaluate the responses from all of the models.

— Jordan Metzner, Episode 22

How it turned out

All four models passed 2 + 2 = 4. Carina then picked Fermat's Little Theorem: for a prime p and any integer a not divisible by p, a^(p−1) ≡ 1 mod p.

So I have a leaderboard. It gave Gemini the best score. ChatGPT is 70, and so on and so forth.

— Jordan Metzner, Episode 22

Gemini scored 98. Carina spotted a problem at 08:22: one answer proved the theorem for natural numbers instead of integers, skipping the negatives. "Just a close miss," she said. That's one problem with one judge, so don't read it as a ranking of the models.

What we'd do differently

• Compile instead of judging. At 07:21 Carina suggested putting each Lean proof into Lean and checking whether it compiles, which should be more painless and more trustworthy than an LLM judge.
• Run thousands of problems. Jordan's idea at 08:40: at enough volume you'd quickly find where each model fails on each problem type. Carina said that's the first thing Axiom did, back when the office was camping chairs and a folding table.
• Reuse the pattern elsewhere. Jordan pointed out the same compare-and-judge setup works outside math, like four models drafting a contract and one picking the best.

For more model matchups, see Claude vs Gemini and ChatGPT vs Gemini.

FAQ

Which LLM is best at math proofs?

In our one real test, Fermat's Little Theorem in Lean 4, the ChatGPT judge gave Gemini 2.5 Pro the top score (98) and ChatGPT's model a 70. That's a single problem with an LLM judge, not a benchmark.

How do you compare LLMs on Lean 4 proofs?

Send the same problem to each model asking for a Lean 4 proof, show the responses side by side with response times, then score them. Jordan used ChatGPT as the judge; Axiom Math's Carina suggested compiling each proof in Lean instead.

Is LLM-as-a-judge reliable for math?

It's a weak basis of truth. Carina pointed out that compiling the Lean proof would be a more reliable check than asking another model, and one high-scoring answer had only proved the theorem for natural numbers, not integers.

How do you build an LLM benchmark leaderboard?

Jordan's app has a problem set of about 10 problems, custom problem submission, run history, a leaderboard from the judge's scores, and an API with user-generated keys so a team can submit problems programmatically.