AI Solved a Hard Maths Problem? What Exactly Was Solved — Sorting the Headlines by Kind, and an Engine That Solves Your Equation and Checks the Answer

Gather last month's Korean headlines and maths looks like a finished subject. "A 90-year-old maths problem, solved by AI in 88 hours." "OpenAI breaks through 300-plus hard problems… Riemann hypothesis proof included." "AI solves a 50-year-old problem in 15 minutes." Yet in the same month, twenty-five Fields medallists signed a statement saying the AI companies' race in mathematics is harming the field. Is one side wrong?

Both are true. But the single word "solved" is covering far too many different jobs. Getting an exam question right, finding a better answer in a search where every answer has a score, digging up a paper that had already solved the problem, and proving a theorem nobody knew: in a headline, all of these become "AI solved a hard problem".

What I set out to do

Three things. First, lay out what solving a maths problem actually involves, and separate the parts AI is genuinely good at helping with. Second, sort the "AI solved maths" announcements from 2023 to now by kind, to see which are real progress and which were inflated. Third, find out how the AIs that solve the Korean CSAT (suneung) or the SAT actually work, and build a small engine that shows the idea. You type an expression in TeX; the engine reads it, decides what kind of problem it is, solves it in textbook order, and checks the answer by plugging it back in.

What it means to solve a maths problem

Exam problems and research problems share the word "problem", but the work is different. An exam problem has an answer, and the setter already knows the route to it. A research problem may not even have an answer. Lay out what a mathematician does, in order, and it looks roughly like this.

1. Choosing a problem — find a question that is both tractable and worth answering
2. Computing small cases — try n=1, 2, 3 by hand or by computer
3. Spotting a pattern and conjecturing — read a pattern in the numbers and write down "probably it's always like this"
4. Hunting for counterexamples — search for cases that break the conjecture
5. Planning a proof — borrow a method that worked on a similar problem, or build a new tool
6. Splitting into lemmas — break the big proof into small steps
7. Checking — make sure no step has a gap
8. Refereeing — other experts read it, often for months
9. Writing it up — so that others can understand it and build on it

This is George Pólya's four phases from How to Solve It (1945) — understand, plan, carry out, look back — stretched out for research. In a 1994 essay, William Thurston argued that the point of mathematics is not proofs themselves but widening human understanding and passing it on. Without step 9, mathematicians don't consider the job done.

The steps people tend to overlook are 7 and 8. Checking is a big share of the work.

• Fermat's Last Theorem: Andrew Wiles announced a proof in June 1993. A gap turned up during refereeing; the idea that closed it came in September 1994, and the paper appeared in 1995
• The Kepler conjecture (the densest way to stack spheres): Thomas Hales submitted a proof in 1998. A panel of about a dozen referees spent nearly four years on it and gave up on a complete check, saying they were "99% certain". Hales started a separate project to have a computer check the proof line by line; it finished in 2014
• The Boolean Pythagorean triples problem: in 2016 a SAT solver (a program that mechanically searches true/false combinations) showed the answer flips at 7,825. It ran on 800 cores for two days, and the proof file is close to 200 TB. A machine has confirmed the answer is right; nobody knows why it is 7,825

So "AI helps with maths" has to be broken down by which of these nine steps it helps with. Steps 2 and 4, computing and hunting for counterexamples, are things computers have done for decades. Step 7 became a machine's job once checkers arrived (formal proof languages such as Lean). Steps 1 and 9 still belong to people. The news in 2026 is in steps 5 and 6: AI has started to build the skeleton of a proof.

The same "solved", five different jobs

Sort the announcements of the past three years by the kind of problem, and you get five strands.

1. Exam problems with known answers

The International Mathematical Olympiad (IMO) is the standard example. In 2024 Google DeepMind's AlphaProof scored 28 out of 42, over the silver-medal line. But people translated the problems into the formal proof language Lean for it, and while students get two sittings of four and a half hours, the AI took up to three days on some problems. In 2025 Google's Gemini Deep Think scored 35 within the same time limit as the students, writing in ordinary language, and passed the gold-medal standard under official IMO grading. OpenAI announced the same score but was not officially graded, and announcing before the closing ceremony caused a row.

These are hard problems. But the setters already know the answers and the solutions.

2. Search scored by a machine

DeepMind's FunSearch (2023) and AlphaEvolve (2025) belong here. The AI writes programs that produce candidates, a pre-written scoring function grades them, and the best-scoring candidates seed the next round. AlphaEvolve found a way to multiply 4×4 complex matrices with 48 multiplications, the first time anyone beat Strassen's 1969 method (49) in that setting. Pointed at more than 50 open problems, it rediscovered the best known results about 75% of the time and improved on them about 20% of the time.

This is the job of "finding a better example". Whether an example beats the record is a single calculation. That is why AI is strongest here. In 2025 Terence Tao and colleagues published a paper running the same tool on 67 problems, and noted that how well it did depended heavily on the hints experts put in the instructions.

3. Finding an answer that already existed

In October 2025 an OpenAI vice-president posted that "GPT-5 solved 10 open Erdős problems" and then deleted it. Thomas Bloom, the mathematician who maintains the problem list, called it "a dramatic misrepresentation". "Open" on his list meant only that he personally didn't know of a paper solving it; GPT-5 had found old papers that already had. DeepMind's Demis Hassabis summed it up in one word: "embarrassing".

Literature search is genuinely useful, and mathematicians welcome it. It just isn't new mathematics.

4. Translating known theorems so a machine can check them

Lean is a language in which a machine checks a proof line by line. Translating a human proof into Lean (formalisation) is notoriously laborious. In 2025 a company called Math Inc announced that its agent had finished, in three weeks, a formalisation of the "strong prime number theorem" that Tao and others had been working on for 18 months. It's a translation of an already-proved theorem, not a new result, but the faster this becomes, the cheaper checking gets for the next strand.

5. Problems nobody had solved

This is where 2026 is different. Through 2025, most "AI cracks hard problem" stories were one of the four above. In 2026 the fifth strand actually showed up.

• Disproof of the unit distance conjecture (May): an OpenAI model broke a conjecture Erdős posed in 1946. Outside mathematicians including Noga Alon, Tim Gowers and Melanie Wood checked it and published their own shorter rewrite
• The cycle double cover conjecture (July): an OpenAI model produced a proof of a 50-year-old graph-theory conjecture, and graph theorists including Jim Geelen and Sang-il Oum of Korea's Institute for Basic Science read it and published expository papers that make it easier to follow

Gowers called the unit-distance disproof a milestone for AI in mathematics. These two are not hype.

Autumn 2026: between the headline and the statement

The trouble came next. Once a few real results had appeared, the announcements that followed started to be reported with the same weight.

Navier–Stokes (September). Whether solutions of the equations describing fluid flow can blow up in finite time is one of the seven problems for which the Clay Institute offers a million dollars. OpenAI announced that it had built an example that blows up; about 10,000 agents reportedly ran for 88 hours. According to Scientific American, the proof concerns a version in which an external force acts on the fluid. The 2000 problem statement includes an option that allows such a force, so it fits the official wording, but most experts have been working on the version without one. Luis Silvestre of the University of Chicago put it this way: "The Clay problem is settled, but the main problem for the Navier-Stokes equations is not." The technique of building a force that makes the solution blow up was itself developed earlier by Diego Córdoba and Luis Martínez-Zoroa.

The 719 manuscripts (October). OpenAI put maths manuscripts produced by an internal model on GitHub all at once. According to the repository's description, about 4,000 problems went in and 372 families of results came out, 719 manuscripts in all, each result taking about three hours on average. About 42% of the top-line results have been machine-checked in Lean, and the README says "some of the unformalized results could have issues".

Among them is a "quasi-Riemann hypothesis" result. The Riemann hypothesis says the (non-trivial) zeros of the zeta function all lie on the line with real part 1/2. The new result says there are no zeros where the real part is greater than 7/8. If it holds up, it gets past a wall nobody has crossed before, which is why some mathematicians said "if a human had done this it would be an instant Fields Medal" — but it is a different statement from the Riemann hypothesis. A human paper building on it has already pushed the bound slightly further, to about 0.87496. In Korean news, it ran as "Riemann hypothesis proof included".

The Fields medallists' statement (September). "A Severe Misalignment of AI in Mathematics", posted on Tao's blog, carries twenty-five names including June Huh, Peter Scholze and Maryna Viazovska. It does not deny that AI can solve hard problems. Its point is that solving a problem is a means and understanding is the goal; it objects to famous problems being used for publicity, rushed out without crediting earlier work and without a write-up others can read. In Korea it was reported as "a warning that AI threatens the human role".

So when you read a 2026 story, three questions are worth asking.

• What exactly was proved? The original problem, or a narrowed version (the forced version, 7/8, a Hodge conjecture limited to special cases)?
• Who checked it, and how? Did outside experts read it, did Lean check it, or has only the announcing company checked it?
• How many out of how many? Is this the pick of 4,000 attempts? Failures don't get announced

Early this year Tao said that only about 1–2% of open Erdős problems are currently easy enough for AI to solve with minimal help. He added that "unsolved for 50 years" can simply mean nobody looked at it for 50 years.

AI is strong where checking is cheap

Put the five strands side by side and a pattern appears. AI won first and won biggest where a machine can cheaply confirm whether a result is right: exams with an answer key, searches with a scoring function, formal proofs judged by the Lean checker. When checking is cheap, failing thousands of times is fine — you try thousands of times and keep only what passes.

Where checking is expensive, the opposite happens: an AI producing lots of convincing wrong proofs is itself a burden. In March 2025 researchers at ETH Zurich had people grade proofs for problems from the US Mathematical Olympiad (USAMO). Models that scored highly on answer-only tests scored very differently once their proofs were graded: Gemini 2.5 Pro got 25%, everyone else under 5%. Writing "QED" confidently after a wrong step was common. Models have improved quickly since, but checking is still expensive. Who is going to read all 719 manuscripts is now a real worry for mathematicians.

Lean looks like it should fix this, but it only fixes half. Lean guarantees "this proof follows from this statement", not "this statement is the question we were asking". The Navier–Stokes dispute happened precisely in that gap.

How the AIs that solve CSAT and SAT problems work

Machines that solve exam problems come from two lineages.

First, the calculator lineage. Computer algebra systems (CAS) such as Mathematica, Wolfram Alpha and Python's SymPy. They hold an expression as a tree and keep 1/3 or √2 exact instead of turning them into decimals, which is what lets them decide whether an expression is exactly zero. Factoring, differentiation, integration and limits are handled by rules and algorithms accumulated over centuries. Apps that solve a problem from a photo usually bolt on formula recognition that turns the picture into text (usually LaTeX). In a 2021 interview, the CTO of Korea's QANDA app said the core, alongside formula recognition, was "search that quickly finds similar problems from a large stock of images, problem-bank style". It finds a similar problem that has already been solved, rather than solving it.

This lineage has a clear limit: it needs an expression to start with. Turning a sentence like "let Q be the point where the tangent at point P on the curve meets the y-axis…" into an equation — modelling — is beyond it. Most of the four-point CSAT questions are decided right there.

Second, the language-model lineage. This one starts by reading sentences. The methods that raised scores since 2022, in order:

• Make it show its work (2022): asking for the steps rather than just the answer sharply raises large models' accuracy
• Solve many times and vote (2022): have it solve the same problem dozens of times and take the most common answer
• Hand the arithmetic to a tool (2022–2023): language models slip on things like carrying in long multiplication, so they set up the equation and call Python or SymPy to do the calculation. The second lineage uses the first as its assistant
• Grade every step (2023): train a separate grader that judges whether each line of the working is right, not just the answer
• Reinforcement learning on answers alone (2024–2025): reward right answers, penalise wrong ones, and let the model learn to write long solutions on its own. Mathematics, where a machine can grade the answer, is a perfect fit

That last method is the direct reason exam-maths scores jumped. Here too, "checking is cheap" is the key. Contests whose answers are integers from 0 to 999, or a CSAT with five-option and short-answer questions, can be graded by a machine, so a model can solve millions of times and reinforce only the paths that got it right.

How about the CSAT itself? Yonhap News, with Professor Kim Siho's team at Yonsei University, gave the 2026 CSAT to free chatbots. Web search was blocked, formulas were typed in LaTeX, and tables and figures were supplied as PDF. ChatGPT (GPT-5) scored 96 in Probability and Statistics, 92 in Calculus and 84 in Geometry. Compare that with the 17 points GPT-3.5 scored on the 2023 exam: three years apart. But of the six questions that EBS and test-prep companies flagged as the hardest, every model got every one wrong, except that ChatGPT got Probability and Statistics question 30 right. DeepSeek also missed an easy question with a table, apparently because it misread the problem.

Researchers from Naver and KAIST built a test from 664 CSAT maths questions from 2014–2025, and attached the official per-question error rates of real test-takers to 339 of them (KCSAT-ML, 2026). The more often people got a question wrong, the more sharply accuracy collapsed for models given little time to think. Given more thinking time, models sometimes overthought easy questions and got them wrong. Apple researchers reported that just changing the numbers in grade-school word problems, or adding one irrelevant sentence, lowers model scores (GSM-Symbolic, 2024). That "AI gets full marks on the CSAT" and "AI can't do the killer questions" can both be in the news at once is because which model and which settings you use changes the outcome a great deal.

The engine I built: it solves, then plugs the answer back in

I built the first lineage — the part that solves once an expression is given. Type an expression in TeX into the box below and press "Solve". The first press takes 10–30 seconds while the engine (Python and SymPy running inside your browser) downloads. Before that, the example buttons show precomputed results straight away.

The engine runs in four stages.

1. Read. It cuts TeX text such as \frac{x^2-4}{x-2} into pieces and builds an expression tree. I wrote the rules for reading textbook notation that drops the multiplication sign — 2x, 3(x+1), \sin 2x — as products. Open "Show the expression tree" and you can see the computer holding division as "multiply by the −1 power" and subtraction as "multiply by −1 and add"
2. Classify. An equals sign means an equation, two or more lines a system, an inequality sign an inequality, \lim a limit, \int an integral, \sum a series. A line starting f(x)=… is taken as a function definition, so the next line can use f'(x) and f(2)
3. Solve. It writes the steps in textbook order. A quadratic is factored if it factors, and otherwise goes through the discriminant and the quadratic formula. A limit is first tried by plugging in; 0/0 goes to cancelling or L'Hôpital, ∞−∞ to the conjugate. The actual algebra (factoring, integrating, finding limits) is done by SymPy; which steps to show, and in what words, are rules I wrote
4. Check. It plugs the answer back into the original. For equations it substitutes each solution and checks left minus right is 0; for definite integrals it compares with a numerical sum over thin slices; for indefinite integrals it differentiates the result; for Σ it compares the formula with adding the terms one by one for n=1, 2, 3 and 7

These four stages are a miniature of the story above. Stage 4 (checking) is far cheaper than stage 3 (solving). And the only reason the engine can say "passed" is stage 4.

Where it went wrong

• It gave only two solutions to a trig equation. For 2\sin x = 1, the first version returned x=π/6 and 5π/6 and declared the check "passed". Both do satisfy the equation, so the check passes. But sine is periodic, so there are infinitely many solutions. The computer algebra system's default solve function returned only representative values. I switched to finding the full solution set over the reals, and added a separate line for "solutions with 0 ≤ x < 2π", as the CSAT asks. A passing check doesn't mean every answer was found. Substituting back only catches wrong answers, not missing ones
• It returned an imaginary solution for an exponential equation. For e^{2x}=e^{x}+2 it gave x=iπ alongside x=ln 2. Solving eˣ=−1 over the complex numbers, that's correct, and it passes the substitution check. But school exponential equations are solved over the reals. For equations that aren't polynomials, it now filters out imaginary solutions and says it did. The machine wasn't wrong; it didn't know the question's assumption
• The answer was right and the explanation wrong. In the extrema example it showed 3x(x−2) = 0 with the note "doesn't factor further over the rationals". It had been handed an expression that was already factored and concluded that "before and after factoring are the same". The solutions x=0, 2 were right and passed the check. Comparing answers or substituting back can't catch this kind of error. It's the same shape of mistake as the language models above that get the answer right but the proof wrong. I made it expand the expression before judging
• It stopped at an absolute value. For |x-3|=2 it gave up with "can't solve". If the symbol x might be complex, |x−3| can't be split into cases. Now, when there's an absolute value, the unknown is taken to be real
• It gave an unreadable answer for a quintic. For x^5-x+1=0 it returned five symbols like "CRootOf(x⁵−x+1, 0)". Not wrong — it means "root number 0 of this equation". There is no general formula for degree 5 and above (the Abel–Ruffini theorem). Now it says so and shows the roots numerically
• The first version couldn't solve a single equation. The table that turns relation symbols into TeX was missing = itself, so inequalities and limits all worked while all five equations ended in an error. Because I'd built a test that runs 26 examples at once before anything else, it showed up immediately

Why one line is enough

Problems where the expression is already given come with rules refined over centuries, and those rules became programs long ago. SymPy is free and open, and there's a tool (Pyodide) that runs it inside a browser. What's left is turning textbook notation into a form the machine can read, writing the steps in the order a person expects, and adding the check. All three are narrow and immediately checkable — exactly the kind of job to give an AI. Building this engine was itself a job where checking is cheap.

If you want to try this yourself

• Set up the equation first. Rather than handing a whole word problem to a language model, write the equation yourself and pass the calculation to an engine like this or Wolfram Alpha; you'll get fewer wrong answers. It's "hand the arithmetic to a tool", done by hand
• Plug the answer back in. Whatever AI you use, the habit of substituting the answer back catches most wrong answers. But substitution won't catch missing ones. For trig equations, equations with roots and rational equations, check the range and conditions separately
• Ask three questions when you read the news. The original problem or a narrowed one? Who checked it? How many out of how many?

What it can't do

• It can't read sentences or pictures. The engine needs an expression to start. For most four-point CSAT questions, setting up the expression is the whole problem
• It can't handle conditions. Problems that split into cases on a parameter, like "the range of k for which there are three real roots", aren't in its classifier yet
• It can't prove anything. It calculates and checks. Showing something "for all n" is not its job
• Its notation is narrow. It can't yet read coordinates (a, b), matrices, vectors or chained inequalities a < x < b. The range for trig equations is fixed at 0 to 2π
• It can't judge where AI mathematics stands. The September–October 2026 announcements are still being checked. Some results may be withdrawn or confirmed after this was written

What mathematicians fear is less AI solving problems than proofs piling up that nobody has read. The solution may come in one click; the checking doesn't yet. That's why, even in this small engine, I built the check before the solution.

If you enjoyed this, please leave a comment.

Sources

• Stages of mathematical work: Pólya, How to Solve It (1945, Princeton University Press) · Thurston, "On proof and progress in mathematics" (1994, arXiv math/9404236)
• Checking case studies: the Kepler conjecture and Flyspeck (Forum of Mathematics, Pi, 2017, Wikipedia) · Boolean Pythagorean triples (arXiv 1605.00723) · Collatz checked to 2⁷¹ (Barina 2025, Brno University of Technology)
• IMO: DeepMind AlphaProof (2024) · Gemini Deep Think gold (2025)
• Search: FunSearch (Nature, 2023) · AlphaEvolve (2025) · Georgiev, Gómez-Serrano, Tao, Wagner (arXiv 2511.02864)
• The Erdős episode: TechCrunch (2025-10-19) · Tao's "1–2%" remark (The Decoder) · AI contributions wiki
• 2026 results: unit-distance disproof verification paper (arXiv 2605.20695) · cycle double cover expositions (Geelen, arXiv 2607.15399; Oum, arXiv 2607.16356) · Navier–Stokes (Scientific American, 2026-09-21, Quanta) · OpenAI maths manuscript repository · paper extending the 7/8 bound (Liu, arXiv 2610.12234) · coverage of the Fields medallists' statement (TechCrunch)
• Korean headlines quoted (in Korean): SBS Biz · Finance Scope (2026-10-08) · Yeosung Economy (2026-05-03, via Daum) · Newsis (2026-09-12)
• Grading proofs: Proof or Bluff (arXiv 2503.21934)
• Exam-maths AI: showing work (arXiv 2201.11903) · voting (arXiv 2203.11171) · tool use: PAL (arXiv 2211.10435), ToRA (arXiv 2309.17452) · step grading (arXiv 2305.20050) · DeepSeek-R1 (arXiv 2501.12948) · GSM-Symbolic (arXiv 2410.05229) · QANDA interview (Byline Network, 2021, in Korean)
• CSAT: Yonhap fact-check (2025-11-15, via Daum, in Korean) · KCSAT-ML (arXiv 2606.10403)
• Engine: SymPy · Pyodide · formula rendering by KaTeX