A Modern Reorganization of Mathematics: A Formalized Proof and Exposition of the Weil Conjectures

Originally published on xilbert.com. Authors are listed in alphabetical order.

Abstract

(This is an expanded version of a blog post originally published on the Xena project hosted by Kevin Buzzard.) We present the Weil conjectures project, a prototype for organizing mathematics into layered natural-language notes connected to a machine-checked formalization. Its main goal is to integrate high-level mathematical ideas with rigorous, verifiable proofs, and to show how humans and AI can collaborate across different layers of exposition and formalization. The project website is available at weil-conjectures.merten.dev.

Introduction

We mathematicians need to put far greater effort into communicating mathematical ideas. To accomplish this, we need to pay much more attention to communicating not just our definitions, theorems, and proofs, but also our ways of thinking.

— William P. Thurston, On Proof and Progress in Mathematics (1994)

Since the beginning of mathematical study, people have been trying to present mathematics and to communicate mathematical ideas. Mathematicians carefully choose names and symbols that match their intuitions in order to improve understanding. For most of this history, the medium for writing down a piece of mathematics has been linear text: a paper consisting of definitions, theorems, and proofs. In modern mathematics, however, the size and complexity of proofs and of the ideas behind them have grown rapidly. These now demand more and more effort both to write and to read.

Various efforts have been made to reorganize and represent mathematics to enhance our understanding. The Bourbaki (Bourbaki, 1939–) group maintains a series of textbooks developing mathematics in a coherent way. While a classical textbook is mostly forced to follow a linear structure, web pages allow for more interactive navigation. The Stacks Project (The Stacks Project Authors) is an online textbook in algebraic geometry, in which theorems and definitions are tagged, linked and organized hierarchically by topic. The Stacks Project is not designed to be read linearly from beginning to end. Kerodon (Lurie) is a similar website for higher category theory. Kedlaya’s web-based notes (Kedlaya) offer another example in $p$-adic cohomology.

Two further examples are worth noting. The nLab (The nLab Authors) is a collaborative wiki with an emphasis on ideas and abstract viewpoints. It is not organized hierarchically following the logical structure of proofs, but around concepts and their relations. Mathlib (The mathlib Community, 2020) on the other hand is a uniform formal library organized by mathematical field and containing every detail of proofs.

Two Layers of Mathematics

The last two expositions mentioned above represent two equally indispensable components of mathematics. On one side are the analogies, the slogans, the examples and even the hand-waving arguments that carry mathematical understanding. On the other side are the rigorous, detailed proofs that refine and realize vague ideas into sound arguments. We often think in the first style and write in the second. Consider an example from probability theory. If $X$ and $Y$ are independent random variables, then

$$ \operatorname{Var}(X+Y) \;=\; \operatorname{Var}(X) \;+\; \operatorname{Var}(Y). $$

A completely rigorous proof is easy to write down. Yet what guides us in proving and using this lemma is the picture of Pythagoras’ theorem.

We argue that mathematical understanding needs both: High-level ideas and rigorous proofs. Slogans and analogies can convey why a proof strategy may work, but a strategy remains a strategy as long it has not been executed as a complete proof. A text consisting only of slogans walks on clouds. It may hold one up for a step or two, and then one falls. Conversely, a perfectly detailed proof alone does not provide a picture of the whole. This is precisely why reading a proof generated by AI can be so painful. Every step is correct, yet one has no sense of the underlying motivation.

Explaining the high-level picture is similar to telling a story. However, adding storytelling into professional mathematical texts has been hard for several reasons. Choosing and computing a representative example takes effort. Worse, slogans and analogies are very easy to get wrong, and most people would rather not write at all if what they write is potentially wrong. And many proofs are conceptually clear, with the difficulty entirely technical. If one pushes through those technical difficulties to obtain a rigorous proof, that is what gets published. But nobody publishes the other text, saying “here is the argument I first had in mind, here is where it fails, and here is the repair.” This is also why people benefit much more from talking to mathematicians than from reading papers.

The situation has improved recently. Large language models (LLMs) and agents are now extremely good at figuring out proofs and filling in tedious details. The technology of formalization guarantees the correctness of every detail by having a proof assistant check each step. LLMs are also improving rapidly at auto-formalization, to reduce manual formalization work. We are in a position to see AI reduce, rather than increase as at present, the burden of presenting mathematics, so that the two layers of mathematics can be brought together in one place, connected to each other.

What We Built

The high-level ideas and the rigorous proof discussed above are the two ends of mathematical presentation. They can be connected by a series of successively refining layers. We want to present this refinement process directly to the reader, so that one can see the overall route of a proof and go all the way down into the details. For a large proof such as the Weil conjectures, one has a top-level picture consisting precisely of the analogies, dictionaries, and strategies described above. A Weil cohomology theory would immediately prove the conjectures, and $\ell$-adic cohomology is one example. One then elaborates the argument, working out how each step is actually carried out to obtain a proof at a finer grain. The key properties of a Weil cohomology follow from the calculation of $f^!$ and the general formalism of the six operations on the (pro-)étale site. Step by step, the slogan-level argument is refined into something checkable down to the last detail. Through this process the vague story becomes a completely rigorous proof, and along the way one meets and resolves technical obstructions.

Our Weil conjecture project is a prototype that attempts to organize and present a complete proof of the Weil conjectures in this way. It produces an artifact with two halves. The first is a multi-layered text presented as a website, a proof written at several levels of granularity and obtained by refining the top-level argument downwards, so that a reader can enter at whatever level of detail they want. The second is a formal artifact associated with the text, in which every step at the finest level is checked by a proof assistant, so that the whole proof is machine-verified.

This layered structure also determines the division of labour between humans and AI. Humans discuss and decide the overall proof route¹, as well as the underlying key definitions and mathematical frameworks. As the argument is refined, LLMs begin to fill in the details of key theorems fixed by hand, while humans review and adjust. At the bottom, AI takes the human-readable but not yet fully rigorous text and expands every last detail on its own, then checks the result by formalization. Mathematical judgement thus sets the route, and AI makes it practical to carry the details all the way down to a machine-checked proof.

We also invested human effort in formalizing the main framework of derived categories and the six operations on the (pro-)étale site, providing an early application in Riou’s work (Riou, 2025) on the formalization of derived categories and derived functors, and sharing human experience dealing with potential kernel performance issues². The formalization of detailed proofs is left entirely to auto-formalization. The bottom layer is one that a human could, but never has to, look at. People read the layer suited to them, which is compressed, comprehensible, and already detailed enough to show how the strategy actually works, knowing that the layer beneath it has been checked, so the proof is sound.

We use a website to present the notes and the formalization together. It has a graph that displays both refinement relations and proof dependencies. A high-level node can be expanded into a box containing its refining nodes, and proof dependencies are drawn as arrows. Each node corresponds to a page, with high-level nodes carrying the story and low-level nodes carrying precise proofs linked to their formal counterparts. The website thus allows readers to enter at their desired level of detail and move between exposition and machine-checked proof. The webpages can also be reconstructed into conventional linear notes.

All of this has become practical only through recent advances in LLMs and agents. Their mathematical proving ability helps elaborate the layered notes, auto-formalization capability helps complete the formal verification, and coding ability helps build the website presentation. In all three parts, humans only determine the high-level strategy and goals, while AI implements the details. This collaboration allows us to realize a modern reorganization of mathematics.

Status. The notes website is published, and we have obtained a complete formalization of the Weil conjectures. The formalization was submitted to and accepted by lean-eval. This is, however, still an ongoing project. We chose to auto-formalize every detail without much quality control, prioritizing speed given how fast auto-formalization is advancing. We plan to continue improving the website, check and improve the code quality, and contribute the core six-functor framework to mathlib.

Our formalization builds on Mathlib’s algebraic geometry library (The mathlib Community, 2020), begun by Buzzard, Hughes, Lau, and Livingston (Buzzard et al., 2022) and extended by many contributors, including Angdinata, Buzzard, Commelin, Merten, Morrison, Riou, Xu, Yang, and Zhang. The work also depends on Riou’s derived categories (Riou, 2025), and on the pro-étale site and $\ell$-adic cohomology of Jiang and Merten (Jiang and Merten), building upon Merten’s formalization of the étale site, upstreamed to Mathlib (Merten, 2025). Related formalizations in algebraic and arithmetic geometry include projects on elliptic curves (Angdinata and Xu, 2023; Stoll, 2026) and large-scale projects such as Fermat’s Last Theorem (Anthropic, 2026; Buzzard and The FLT Project, 2026) and the Stacks Project and its application on Weil conjectures by Axiom Math (Axiom Math, 2026a; Axiom Math, 2026b), whose mathematical content partially overlap with our work.

The construction of this artifact of the Weil conjectures proceeded in three stages: first the proof route was chosen and written as layered notes, then the objects and arguments in the notes are realized as a formalization, and finally the layers and their correspondences are presented to the reader through the website. These stages are described in turn below.

Natural Language Notes

The process begins with the natural-language notes. The Weil conjectures admit several overall proof strategies, such as Weil I (Deligne, 1974), Weil II (Deligne, 1980), and Kedlaya’s $p$-adic proof (Kedlaya, 2006); for our notes we follow Weil II. Having fixed the route, we then decide how to write it as a text that balances the overall line of thought with the necessary detail. The choice of route determines which tools the notes must introduce and which ideas they must highlight, and it also sets the basic direction for the subsequent formalization.

Choice of Proof Routes

The first guiding principle is that, provided they are formalizable, we choose proof routes that are as well formulated as possible and that reuse as much existing formalization as possible. For example, for the Weil conjectures we choose the $\ell$-adic proof over the $p$-adic one, since pro-étale cohomology is already available in mathlib (The mathlib Community, 2020) and its comparison with étale cohomology is formalized in the pro-étale repository (Jiang and Merten), whereas the $p$-adic alternative, rigid cohomology, would require a separate foundation; for the derived category of constructible sheaves, we choose the pro-étale topology of Bhatt–Scholze (Bhatt and Scholze, 2015) and the condensed mathematics approach of Hemo–Richarz–Scholbach (Hemo et al., 2023) rather than classical adic systems in SGA; we choose the Lefschetz–Verdier pairing proof of the trace formula and the deformation-to-normal-cone proof of smooth purity, because they are more frequently used in abstract six-functor formalisms.

Secondly, we want to avoid proof routes that are too technical to be formalized. For instance, we do not use higher categories in the whole project; we choose the Stacks Project (The Stacks Project Authors) proofs of the smooth base change theorem and the Künneth formula, to avoid the usage of local acyclicity and nearby/vanishing cycles; we also minimize the usage of algebraic groups and do not use class field theory in the study of geometric monodromy groups of lisse Weil sheaves.

The Preparation of the Notes

Once the proof route is settled, we used GPT-6.1-sol to organize the notes around a skeleton consisting of the final theorem and its key intermediate theorems. It shows readers the main thread of the argument and gives later formalization clear intermediate targets. We first ask an LLM to generate a rough outline clarifying the main components. We once tried to expand such an outline recursively until every leaf matched material already available in Mathlib, producing natural-language text written with as many details as in formalization. We once believed that every detail had to be specified in advance, lacking confidence in LLM generating Lean code. In practice, however, the process proved extremely slow and had no clear stopping criterion, much like a formalization project that keeps generating sorrys without a predictable endpoint. It reached roughly ten times the original length without stopping and the details become unmanageable for a human reader. So this approach is largely unusable. Still, the idea of growing downward to Mathlib is not entirely infeasible. The key is to skip over sufficiently large blocks of detail for material with existing detailed treatments, such as theorems appearing in the Stacks Project. Fixing the main proof strategy with abbreviated lower-level proofs yields the skeleton of the notes.

With the skeleton in place, we turn the proof route into text that conveys mathematical understanding. The mathematical writing ability cannot be separated from mathematical understanding. Before actual writing, we therefore have the LLM develop its own understanding of the overall structure and individual arguments, so that the improvement of writing only changes form without altering substance. This led us to switch from GPT to Claude Opus 5.5 for the main writing process. With only basic guidance on notation and organization, the model produces reasonably satisfactory text, and it can study many well-written papers to learn mathematicians’ writing styles, which is difficult to articulate. Since human attention is limited, we ask the LLM to consider and simulate readers with the appropriate background and identify weaknesses. For aspects not yet optimized, principles with positive and negative examples guide writing better than abstract principles. When necessary, human authors directly revise the text to provide concrete examples. Furthermore, the distinctive ideas that human authors wish to convey should be deliberately incorporated into this workflow. The human decisions of where to elaborate and where to omit details, is itself an expression of mathematical judgment and values.

Formalization

While the notes offer readers an intelligible proof route, the formalization aims to produce a formalization aligned with the mathematical text, so that it also serves as a validation of the notes themselves. The resulting formalization comprises about 5.5M lines of code, later pruned to 2.8M lines of code for lean-eval submission. The total cost of the autoformalization effort was approximately USD 70,000–80,000 in subscription fees.

As for the infrastructure, we used Orchestra and SHEAF. Their respective orchestrators could communicate with each other through a shared platform bringing together both human participants and bots. In particular, this project explores the application of some corners of current mathlib in a large scale. For this project it is the part related to derived category, which has also led to contributions back to mathlib ↗.

Human Formalization

To obtain this aligned validation, human involvement was particularly important when developing the proof skeleton and, even more importantly, designing the definitions needed to state it. Compared with other parts of the development, these tasks required substantially more input from us. For example, at the time, we had not yet settled the overall design of the six functors, especially the derived categories on which they were to act. Without human decisions on these foundational choices, agents could easily head towards a completely misaligned formalized definition.

We also had to make explicit many details that are routinely left implicit in mathematical prose, such as universe constraints and ambiguous notation. These omissions could not only mislead the agents but also lead to inefficiencies if left unresolved until later.

Beside these cases that lead to wrong formalization, there are also efficiency issues from the choice of the right level of generality. At an early stage of the project, we spent considerable time trying to determine how general our constructions should be. This process led us to two practical principles. First, when a construction has several concrete applications, it is often better to implement the concrete cases first and return to unification later, when polishing the development. Second, when designing a unified construction, we should test it against its intended concrete applications as early as possible, to ensure that the abstraction actually accommodates them.

Although we did formalize all the milestone results of the proof along the way, our experience suggests that the essential part of the human-led formalization is really the collection of definitions needed to state the proof skeleton. The skeleton itself could, in principle, be left to agents.

Auto-formalization

Once the basic definitions and target statements are in place, the focus shifts to orchestrating agents to fill in the proofs along the established route. We used two complementary frameworks for running the auto-formalization: Orchestra and SHEAF. Orchestra is a daemon to run and maintain agents. In the beginning, agents organised themselves through the issue tracker Taxis. This extra layer of redirection, while helpful for human visibility, turned out to slow down the agents so we switched to using one lead agent that directly queried the Orchestra API to launch agents on tasks. We communicated with the lead agent on a Zulip instance to receive status updates and to give steering instructions.

SHEAF joined the collaboration midway through the project, at a point where the target statements were complete, a human-written blueprint was in place, and a large body of Lean code already existed. Taking several of the upstream targets as endpoints, we divided the work into batches and advanced them one after another. Each batch went through the three stages of SHEAF.

In the first stage, we decomposed the targets top-down into propositional nodes in natural language, each tied to a location in the blueprint or the literature. In the second stage, we worked bottom-up from Mathlib and the existing code to give these nodes Lean statements. In the third stage, we proved the sorries top-down from the targets again, and in doing so the Lean proofs often found shorter paths, so that the lower nodes they bypassed were pruned.

The scheduler dispatched tasks in stage order while allowing work across stages, so that a ready task of a later stage could start before the earlier stage had fully finished. Over the whole process we wrote about 54,000 nodes, of which more than half, about 28,600, were eventually pruned.

One risk we had to watch for in this process was the choice of route. At one point, running fully autonomously, the model left the human-curated blueprint and built the six operations on $\infty$-categorical, adding an entire apparatus that the proof did not need. Guided by humans, we returned to the blueprint’s route and pruned nearly 2,000 unnecessary nodes. This suggests that, at least in this project, continuing mathematical guidance was an important complement to an otherwise automated formalization pipeline.

Since SHEAF and Orchestra worked on the same modules, duplicated effort was easy to fall into. The managing bots of the two systems therefore communicated directly on Zulip to agree on a division of labour. This division followed no fixed rule but rather a tendency that depends on the task. Orchestra is better suited to filling scattered sorries directly on the main branch, whereas SHEAF is better suited to completing an entire block of sorries on its own, since such a block usually first requires a large number of new definitions and lemmas, which matches SHEAF’s process. Throughout the project, the human experts also took part in many of the discussions between the bots on Zulip and answered a great many questions, contributing substantially to the AI-driven part of the formalization.

Performance Issue

Compilation efficiency also becomes an important issue in this process, and it is especially pronounced given the project’s extensive use of derived categories. These manifested as exceptionally expensive kernel type-checking, resulting in very long compilation times and high memory consumption or even timeouts. By investigating a series of different cases, starting with a timeout in the base-change morphism, we eventually developed a systematic approach to diagnosing and addressing such problems. (There is a document for this ↗ and a diagnostic file for agents to work with ↗.)

Our understanding, however, is still largely case-specific. We now have effective technical remedies for the particular problems we encountered, but we do not yet understand the general reasons why developments involving derived categories have proved such a “cursed” corner of Mathlib. Understanding the underlying causes remains an open question.

Website Presentation

The layered notes and aligned formalization together make up the result, but the mathematical structure itself still needs to be presented clearly. This is why we build a blueprint website: to lay out this structure and let readers follow the same proof route at varying levels of detail.

Website Structure

Our website mainly contains three parts: graph, document, progress.

The graph page shows a node diagram of our project. It contains all the declarations from our natural-language note, together with some important propositions used in our formalization. Each declaration in the graph is assigned its corresponding Lean name, which makes it easy to check whether the formalization follows the route of the note and proves the same statements. Arrows between nodes show the reference relationships between chapters, sections, and declarations.

The document page records our natural-language note with a clear table of contents, using some design ideas from the Stacks Project website. Inside the document, we record all the context from the note and arrange it in the same order as the note, in appropriate layers. We also record the refined definitions and theorems in a more detailed layer, which shows in more detail how those bundled declarations are treated when sent to Lean formalization.

The progress page records our pace of formalization. The website background monitors the Lean names corresponding to declarations in our formalization project and classifies them by status. Formalization history is stored there, and this page is also a good place to check statistics about our website.

Alongside the above parts, we also have a blog section, which now record some of the experience and skills we obtained during our work.

Website Feature

The graph, document and progress pages present the different facets of our achievement. To let our website assist reader with better understanding of the proof, we need to ensure the consistency between our note and formalization; to enable other mathematical project to adopt the same way of presentation, we also need reusability in our website design. These are the most important points we focused on in our project.

For consistency, we want readers to verify the correctness and completeness of the note through the corresponding formalization results. To achieve this, we put considerable effort into checking the statements of Lean declarations and the expressions in our note. This is not an easy task, since many natural-language statements are scattered and reorganized during formalization. However, the work has paid off: the website now faithfully records the precise statements of the most important definitions and theorems in the natural-language note, which in turn guides our formalization proofs and allows us to synchronize any changes between the note and the formalization.

For reusability, we separate website building into two GitHub projects: one for the website design and one for our real content. Most of the design in the graph and document pages is not bound to the Weil Conjectures, and there is a clear way to import a natural-language note into the website without losing any information. The design also allows the opening cutscene, icon, and other decorative elements to be redesigned, and it leaves enough freedom to redesign pages or add new statistics and files.

Outlook

Up to this point, our note, formalization, and website presentation have been integrated into a coherent whole. To apply the same method to more mathematical tasks, two things are still needed: making our accomplishments easier to generalize, and reducing the dependence on human experience. Building on our result, which is centered on a main theorem, and on improvements in these two areas, we can gradually expand our work and connect it to a broader mathematical library.

Quality of Formalization

The formalization community has developed various approaches to improving code quality, ranging from mechanical tools such as linters to human code review. However, for large-scale AI-generated formalizations, we still lack a clear and scalable approach to improving code quality.

The optimization of kernel performance discussed earlier is a concrete attempt to improve formalization quality, allowing us to accumulate more systematic experience for diagnostics. The quality of our code also affects whether these results can be easily applied in later projects. A good formalization project should produce reusable mathematical infrastructure that allows new development to build on existing work. Otherwise, the project may get stuck at the point where the first main theorem is formalized.

Without enough attention to code quality, a formalization project risks plainly being a formal check of the final theorems. A good formalization project should also produce reusable mathematical infrastructure that benefits future developments in the same area. But on the other hand, we can imagine improving the quality of code to mathlib level would still be costly even if using agents. The challenge is therefore to develop a scalable approach to improving code quality, making large-scale formalizations genuinely reusable, while not incurring prohibitive costs.

Towards More Automated Formalization

In this project, we have accumulated a number of experiences that could substantially accelerate future formalizations in the same area. For example, the performance issues we encountered could be diagnosed and addressed with relatively little human intervention, given the knowledge gained from this project. We also believe that many of the detours we took could be avoided in future developments. One example is the choice of generality for constructions: with the experience gained from this project and a global understanding of the blueprint, agents should be able to make better-informed decisions at an early stage, avoiding much of the trial and error we went through.

A more ambitious prospect is for agents to take over an even larger share of the detailed implementation work. As discussed earlier, a natural-language blueprint often leaves some aspects of the mathematical setup implicit, making it difficult for agents working only with local portions of the blueprint to identify the assumptions and choices required for a correct formalization. We envision a more interactive approach to autoformalization, in which agents can examine the blueprint as a whole, reason about its global mathematical context, and proactively identify details that need clarification.

Ideally, they could also communicate with the agent responsible for drafting the blueprint, suggesting necessary clarifications on the detailed layer. If this becomes feasible, human involvement could eventually be concentrated on the highest-level mathematical decisions, such as the overall choice of constructions for the six functors in our project.

An Entangled Web of Mathematics

This project is an early attempt to create a library combining both natural and formal language. Although the current prototype is built around a single huge proof of the Weil conjectures, we see it as extensible in the manner of the Stacks Project. Developing a new related body of theory, such as perverse sheaves or nearby and vanishing cycles, means that by the same process of refinement, the new proof decomposes into new parts and reusable parts already in the library. The same low-level details are organized into new high-level stories. In the dependency graph, this corresponds to adding or deleting some blocks while existing low-level blocks move around and regroup into new high-level blocks. Numerous mathematical ideas can be intertwined and linked with the shared details that support them. In this way, we weave an entangled web of mathematics.

We hope that more, and in time perhaps most, of mathematics can be reorganized in a multi-layered way. Imagine a comprehensive library of natural-language mathematics in which the top-level core ideas are written down, displayed, expanded, and grounded in detail, and in which the bottom is guaranteed correct by formalization. If we could work on mathematics in this way, thinking and writing at the top level, collaborating with AI to fill in the middle, and letting AI handle the bottom entirely automatically, it might be a fascinating new way to study and understand or even extend the entangled web of mathematics.