For over a century, the Thomson problem has asked a deceptively simple question: how should repelling charges arrange themselves on a sphere to minimize energy? This week, ten instances of Claude Sonnet 5.5 did what no human had done with a computer-checked proof — they solved the seven-charge case with a 17,895-line Lean proof, verified by two independent kernels.

It’s a striking milestone: AI not only generated the mathematics but also produced a formal proof machine-checked line by line, removing the need to trust a human’s judgment.

What Happened

In 1904, J.J. Thomson posed the problem while trying to understand where electrons sit inside an atom. Though his atomic model was later abandoned, the geometric question became a classic headache in mathematical physics. Exact, computer-verified answers exist for only a handful of cases — and seven charges was one of the gaps.

Vals AI set ten instances of Anthropic’s Claude Sonnet 5.5 on the problem. Over 15 hours, the agents traded 1,270 messages and produced a 17,895-line Lean proof covering the seven-charge case. Two independent kernel checks confirmed the work. The GitHub repository itself flags the proof as not peer-reviewed, but the formal verification speaks loudly: every step was checked by software.

This is more than a stunt. The Thomson problem is a concrete, well-defined challenge where AI produced a verifiable result in a formal system. No hand-waving, no “reasoning errors” hidden in a wall of prose — just a machine-readable proof that can be inspected by anyone.

Read the full announcement →

My Take

This matters because formal verification eliminates the biggest risk in AI-generated mathematics: hallucination. An LLM can generate a plausible-looking argument that falls apart on inspection; a Lean proof cannot survive a kernel check. That’s why this result feels different from earlier AI math demos. Claude didn’t just conjecture an answer — it constructed a formal derivation that no human had to “trust.”

For developers and researchers, this is also a signal about how to use AI in high-stakes reasoning. The agents weren’t asked to write an essay about the Thomson problem; they were asked to produce something a compiler could check. That’s a template for reliable AI in scientific computing, formal verification, and any domain where correctness is non-negotiable.

Of course, the work isn’t peer-reviewed yet, and the proof itself is sprawling — likely not something a human would write. But that’s almost the point: AI is beginning to produce results that are both beyond human speed and beyond human trust, as long as we have the tools to verify them.

What to Watch

  • More AI-generated formal proofs in open problems — the Thomson problem is a test case; expect harder questions to follow.
  • Rising value of formal verification infrastructure — kernels like Lean will become a critical safety layer for AI reasoning.
  • New division of labor between AI and humans — AI proposes, the kernel disposes, and humans set the agenda.