Clawristotle: Semi-Autonomous Mathematical Research
Fully verified formalizations of research-level mathematics in Lean 4, produced by centaur teams of AI agents and human mathematicians.
This repository hosts two completed formalization projects. Each is a self-contained Lean 4 / Mathlib package in its own directory, with its own toolchain, README, and technical report.
landau/ | grothendieck-vanishing/ | |
|---|---|---|
| Theorem | Positive smooth steady states of the Vlasov–Maxwell–Landau system on 𝕋³ are global Maxwellians (Guo–Strain, Theorem 42) | For a Noetherian topological space X of dimension n and any sheaf F of abelian groups, Hⁱ(X, F) = 0 for i > n (Hartshorne III, 2.7) |
| Status | ✅ Fully verified, 0 sorry's | ✅ Fully verified, 0 sorry's, no extra axioms |
| Lean 4 code | 10,445 lines | 5,061 lines (4,087 normalized) |
| Timeline | 10 days (Mar 1–10, 2026) | 35 days (Mar 27 – May 1, 2026) |
| API cost | ~$6,300 | ~$15,000 |
| Agents | Claude Code · Gemini DeepThink · Aristotle | Claude Code · Codex CLI · Aristotle |
| Paper | arXiv:2603.15929 · HF paper | Technical report |
| Read more | README · Technical report · Blueprint | README · Brian's review · Blueprint |
How it works
The human steers — choosing the theorem, fixing the definitions, auditing the final statement — while AI agents handle the implementation: writing the Lean code, searching for proofs, dispatching hard lemmas to the Aristotle cloud prover, and reviewing their own output in autonomous critique–plan–prove–simplify loops. Each project's README describes its agent stack and how the method evolved between the two projects.
Working in this repository
Each project is an independent Lake package with its own lean-toolchain — build from inside its directory:
cd landau # or grothendieck-vanishing
lake exe cache get # fetch the Mathlib build cache
lake build
The Landau project was developed first, on this repository's main branch (March 2026); the Grothendieck vanishing project followed on the grothendieck-vanishing branch (March–May 2026) and was merged into main with full history.
License
Released under the Apache License 2.0.