Your model runs faster on hardware that stays local.
The harness compiles to your exact hardware and wraps the model you already run. Every proof it produces is checked by the Lean kernel.
Imagine that every time you read a book, you had to start at the beginning for every new word in the story. By the last page of a 200-page novel, you would have read the book sixty thousand times.
That is autoregression. It is the architecture under every frontier AI model in production. The cost of an answer scales with the square of the answer's length. Doubling the response quadruples the bill, and the curve cannot be flattened by paying for a faster chip.
We believe there is a better way.
A small team took up a theory that looked too impossible to finish: if every piece of software can be written in math, can every piece of language?
We started with our own library of atoms, apart from mathlib4. In May it held 4,000. Seven weeks later, over 31,000. Each new atom proves faster because it stands on the ones already proven.
Emails, messages, and medical records stay inside the perimeter where they started. The harness reads the book once, so the hardware you own carries more of the work.
Apple took IBM's mainframe and put it on the desk. What lived in the data center is moving again.
Ten results, 249 pages, no proof assistant.
OpenAI has released a collection of results obtained by an internal model, spanning mathematics and theoretical computer science. Among them the first improvement to the general sphere-packing exponent since 1978, a counterexample to Connes’s rigidity conjecture, and an explicit non-sofic group.
Across all 249 pages there is no occurrence of Lean, mathlib, Coq, Isabelle, or any machine-checked step. Every result reaches the field as informal mathematics and waits on human referees.
No frontier lab ships machine-checked proof at this scale, because the tooling to do it does not exist yet. Refereeing takes months and does not parallelize. Producing candidate mathematics now does, and the distance between the two widens with every model generation.
A Lean kernel checks a proof term in the time it takes to compile it and never asks which model wrote the candidate, which is why verification is the layer that scales.
Most AI is frozen the day training ends. The model answering you now is the model as it was months ago, and moving it forward means training it again at the cost of the first time.
Our engine separates the model from what it knows. The foundation model stays stable while the library grows beneath it as a content-addressed hypergraph: atoms, proofs, corrective hints, and the rules that compose them. New facts enter as versioned nodes and typed hyperedges, and a DAG projection over the graph gives deterministic dependency order, replay, and impact analysis. The graph is append-only, so nothing already proven is overwritten.
Reasoning improves at two speeds. Immediately, through retrieval over the graph, so a lemma proven this morning is in play this afternoon with no weight change at all. Then, more slowly, through guarded distillation and adapters with regression replay, so new capability folds in without erasing the old, the failure mode called catastrophic forgetting.
The proven atoms do not drift. What grows is the engine's skill at finding and composing them.
Eight programs, one finding.
Diffusion competes at base scale and loses to autoregression in the regime that decides real work: post-training and proof correctness. We designed our engine around this record.
Apple ML Research
Beat autoregression at base (67.1 vs 61.6 HumanEval), then lost 18 points after instruction tuning (72.0 vs 90.2). Post-training regressed.
DeepSeek-AI
The strongest public Lean prover stayed autoregressive (88.9% MiniF2F). No diffusion proof system posted a correctness number at all.
Google DeepMind
Up to 4x faster than autoregression, with no frontier-quality or proof-correctness result. Speed only.
ByteDance Seed
2,146 tokens per second throughput, with no verifier loop and no win over matched autoregression under formal constraints.
NVIDIA Research
Pure diffusion was insufficient. The deployable result kept autoregression in the loop as a tri-mode hybrid.
Inception Labs
Reached parity with autoregression on code (76.2 vs 77.6 GPT-4o), not a lead, and showed nothing on correctness or post-training stability.
HKU NLP / Huawei Noah's Ark
Competitive but below frontier (21.4% LiveCodeBench) and dependent on autoregressive initialization. No proof-grade result.
HKU NLP / DreamLM
Fixed-canvas fix for code infilling, unproven on Lean proof spans. Not yet an autoregression-beating result in the proof domain.
We designed Lemma around this record: a Lean verifier as the floor, an autoregressive control as the baseline, and diffusion only where it beats that control.
A recursion cited since 1973, on the strength of two words.
Chapter 9 of that same document closes a problem opened in 1973, proving Rk(3) = kΘ(k) and settling the Erdős question of whether the limit is finite. Chung is cited in it.
Chung’s paper gives f(4) ≥ 50 and the recursion f(k+1) ≥ 3f(k) + f(k−2). The k = 4 case is proved by hand, seven cases with sub-cases, on an explicit 50 × 50 matrix. The general case is a diagram and the sentence that its proof is quite similar to the one before it.
That general diagram introduces a block with no counterpart in the k = 4 construction, so it is not the same argument with more indices. The step is load-bearing for every citation the recursion has collected since, and it was never written out.
Checking it is a decidable finite computation. We are running it against the kernel.
Result pending.
What is the difference between a traditional LLM and Lean 4 as a coding language?
A coding language that only knows math, free of the complexity of probabilistic language, is a very powerful calculator. That calculator belongs on your device.
import Mathlib).
A technical due-diligence packet is available on request.
For more information, please contact us. Full data room access is available to qualified entities.