Jonathan Laurent

Researcher in machine learning and automated theorem proving | CMU PhD

[Jonathan Laurent @jonath_laurent]

Using the Stacks formalization we built at Axiom, we formalized the Weil conjectures in a single day. With the foundations in place, formalizing research-level algebraic geometry is now within reach for anyone working in the field.

[Axiom @axiommathai]

We shared our formalization of Stacks. Is it reusable?

The true test of a foundational library is what you can build on it.

Now, we release the Lean formalization of the proof of the renowned Weil conjectures (I-IV), one of which gives Riemann Hypothesis over finite fields. ✨

[Axiom @axiommathai]

Read more about the Stacks story:

"Axiom also trained its own models to be good at math, an approach Hong said most other verification startups haven’t taken."

Axiom is betting that the software of the future will need to rest on verified foundations, the way Stacks now does.

[Talia Ringer 🕊🪬 @TaliaRinger]

I really love that any company is thinking about good proof engineering. Carina read the literature on this and it shows. And they hired some great people who also know the literature (I'm biased since one of my students is still there)

[Alexander Terenin @avt_im]

Andrej Karpathy’s famous blog post about RNNs famously had an example RNN trained on the original Stacks Project’s LaTeX source.

This mountain of work has now been formalized in Lean!

[Przemek Chojecki | PC @prz_chojecki]

Formalization of the Stacks Project through a swarm of AI agents marks for me the end of the DeepAlgebra project.

In 2016, 10 years ago in pre-LLM times, I wrote this funny short paper called DeepAlgebra (link: https://t.co/5Yn5gbo8eO) on how one could approach semi-automatic formalization of the Stacks projects with hammers (!) and deep learning.

It might have been pretty naive in retrospect but it pushed me from pure math towards AI. And here we are - 10 years later - the Stacks Project is formalized. Congrats to the Axiom team!

[Tony Feng @tonylfeng]

I'm impressed by @axiommathai's formalization of the Stacks Project! To be clear, there was never any doubt about the correctness of this (human-written) mathematics. But with CSFG and now Stacks, Axiom Math has done a good job of identifying formalization projects which are useful for the community.

My suggestions to continue this trend: formalize the proof of the Geometric Langlands Conjecture, and the theory of Kuranishi structures!

[Jonathan Laurent @jonath_laurent]

@viest_w @axiommathai It builds on Mathlib! In particular, the definition of sheaves is taken from there: https://t.co/GvOSLiI2YO

[Jonathan Laurent @jonath_laurent]

We just released the Stacks library, a foundation to build on! For starters, 483 formalization tasks are open for contributors: https://t.co/UjV7vga6YS

[Axiom @axiommathai]

Most think vibecoding at scale is slop. Here’s a counterexample.

Today we release a 16M-line formalization of the entire Stacks Project, critical infra underlying modern math, with optimized code quality and its highly interconnected structure preserved.

A mathematical city 🌆

[Tianfu Fu @TianfuF]

I still remember my modern algebra professor telling us that the classification of finite simple groups took decades and over 10k pages of proofs.

No one had really verified the whole thing end to end. There could even be hidden circular dependencies that nobody had noticed. That uncertainty had always made mathematicians a little uneasy.

But who would sacrifice 10 years of their academic career just to audit someone else’s proofs?

It’s incredibly exciting to see AI making this kind of verification possible.

Hopefully AI can finally settle the ABC Conjecture controversy next!

[Axiom @axiommathai]

The largest math proof in human history is now computer-verified.

Today, Axiom announces a complete Lean auto-formalization of the Classification of Finite Simple Groups, the "periodic table of symmetry."

About 15,000 pages, built by over 100 mathematicians across generations.

[Jonathan Laurent @jonath_laurent]

Axiom's agent swarm was writing Lean faster than it could compile, so build times turned into the bottleneck and a whole distributed build cache had to get built to keep up.

[Leo @biosemiote]

The formal proof of CFSG may now be among the largest open-source projects ever. Watching agents assemble it is a reminder of the awe-inspiring human achievement behind it. The graph represents some 15,000 pages of intricate arguments developed by mathematicians over decades.

[Jonathan Laurent @jonath_laurent]

In 2012, a pioneering team from @Inria led by Georges Gonthier formalized Feit-Thompson in 170K lines of Rocq, a pillar of the classification of finite simple groups.

In their footsteps, @axiommathai formalized the entire classification in 43M lines of Lean, with an AI swarm.

[Axiom @axiommathai]

The largest math proof in human history is now computer-verified.

Today, Axiom announces a complete Lean auto-formalization of the Classification of Finite Simple Groups, the "periodic table of symmetry."

About 15,000 pages, built by over 100 mathematicians across generations.

[Jonathan Laurent @jonath_laurent]

@EternitiesAI @axiommathai And let's not forget the Baby Monster!

[Jonathan Laurent @jonath_laurent]

@ragzoi @svpino Lean build times becoming the bottleneck wasn't on our 2026 bingo card!

[Jonathan Laurent @jonath_laurent]

@guillaumeclaret @axiommathai Yes, the work spans over more than 500 books and articles!

[Jonathan Laurent @jonath_laurent]

@HelloVyom @axiommathai We published a paper on this!
https://t.co/1DrwnR9qmH

[Jonathan Laurent @jonath_laurent]

@BasMondragon @axiommathai Humans only audit the theorem statement. And verified checkers are coming: https://t.co/xnWi394Fp3

[Jonathan Laurent @jonath_laurent]

@themarklstone @kevinweil @axiommathai Verified kernels are coming: https://t.co/xnWi394Fp3

[Jonathan Laurent @jonath_laurent]

@mktpavlenko @axiommathai Great observation! Our formalization effort reused the statement from the Tau Ceti project:

https://t.co/ZKvhGtLo7j

Note that it is tiny compared to the formal proof and can easily be audited by a human.