the lean bottleneck.

The labs racing to build theorem-proving models — Harmonic, Axiom, Logical Intelligence — have raised hundreds of millions of dollars on a single bet: that closed-loop reasoning models verified by formal proof are the next frontier. They are right.

They are also stuck. Not on compute. Not on architecture. On people. Mathlib — the Lean library every autoformalizing model depends on — does not scale at the rate the models need it to, because the set of humans who can extend it is small enough to fit in a single Telegram group. The bottleneck is not data. It is expertise.

We build the supply side. Desargues trains Lean experts and routes them to the labs that need them. Mercor for formal verification, supply side first.

Three things make this winnable from where we stand. Twenty years of IMO and IOI network out of Kazakhstan — our first experts are people we sat next to on national teams. Six months inside the formal-reasoning community, watching mathlib4 reviewers repeat the same notes across PRs (the retriever at /tool is one artifact from that period, free for the community). And working relationships with the senior figures of the Lean community — the people who have spent the last decade convincing pure mathematicians that formalization is worth their time, and who are helping us build the supply side correctly.

Mathlib is the entry point, not the destination. Once the supply side reaches scale on formal math, the same machinery extends to quantitative finance, software verification, and smart contracts — every domain where a closed-loop reasoning model needs a verifier and a corpus that does not yet exist.

We are early. We won the MBZUAI hackathon — 1 of 900 teams, against DeepMind, MIT, Harvard — by shipping our autoformalizer in a weekend. The next milestone is the first paying lab.