eRacks Systems Tech Blog
Open Source Experts Since 1999
An AI Just Proved Fermat’s Last Theorem. Here Is What That Means for the Server You Buy Next
On September 4, Anthropic published the first complete, computer-checked proof of Fermat’s Last Theorem. Claude wrote it in Lean, a programming language built so a computer can verify every step of a mathematical argument instead of a human reviewer. Eleven days, largely on its own, 13 million lines, about 29,500 intermediate theorems along the way, and nothing assumed beyond Lean’s three standard axioms. Andrew Wiles’s 1995 proof ran 129 pages and took months of expert review to check.
I read that as a hardware story.
Eleven days of work, not a chat reply
The interesting part is not that a model knew number theory. It is that a machine did eleven days of sustained, structured work, and another machine checked every line of it. That is the shape of job we spec servers for now: long-running agents that read, write, test and retry against your own documents and code, not a question-and-answer box.
The frontier models live in their makers’ datacenters. What you can own is the open-weight class right behind them (Qwen, Llama, DeepSeek, Gemma), running on hardware you control, on your own documents, with no per-token bill and nothing leaving the building.
What that class of model does on a server you can buy
On our bench, a dual Intel Arc Pro B70 server runs Qwen3-14B at 54 tokens per second and Qwen3.6-27B at 26 (a token is about three quarters of a word), with the models resident in 64GB of GPU memory. The measurements, the software stack and the three power-management fixes it took to get there are in our benchmark write-up.
The money
Run the arithmetic our public rent-versus-own calculator uses (24 hours a day, 15 cents per kWh, $1,200 a year of overhead, a three-year payback) and an eRacks/AINSLEY at $21,395 pencils out against an AI bill of about $800 a month. A team of ten on $100 seats is $1,000 a month, forever. The calculator takes your own numbers, and every field is editable.
Every eRacks server is built to order, burned in, and benchmarked before it ships, with the numbers in the box. If you are sizing a machine for this kind of work, the AINSLEY configurator is the place to start, and a quote request gets a reply within one business day.
Joseph Wolff, Founder and CTO, eRacks Open Source Systems
joe September 9th, 2026
Posted In: AI Servers, News
Tags: AI server cost, eRacks/AINSLEY, Fermat's Last Theorem, formal verification, Intel Arc Pro B70, Lean, on-premise LLM, private AI, Qwen3