Within a decade or two, mathematics might look completely different. Around 2036, the first generation of AI-native mathematicians ― mathematicians who underwent their training with powerful AI accessible ― will become faculty members. I also expect AIs being able to autonomously produce Annals-level papers within 2-3 years, possibly earlier than that.

Below is one way things could turn out. I’m no fan of sci-fi, but using the conditional everywhere in the narrative was inconvenient. So here goes.

The community #

Already in 2026, most research took place online. Over the last few decades, research-level mathematics had become increasingly specialised, with mathematicians spending more time in Zoom calls and online forums.

What defines a research community today is no longer the blackboard discussions during coffee breaks at conferences. Even a relatively niche field like p-adic Hodge theory can’t gather all key contributors: once the digitalisation of mathematics became cheap and scalable, with autoformalisation agents writing Lean code up to Mathlib standards, small research communities grew tenfold in size. This led to unprecedented progress: people with no formal background in mathematics made significant breakthroughs, which were then merged into the wider research program. Indeed, these days, research communities are primarily defined by shared GitHub repos, all following a similar structure.

The most important repository holds the canon, a collection of foundational texts considered worthy of study: scanned PDF versions of historical texts from the 20th century, expositions of the field’s most beautiful results, biographies of prominent mathematicians. The proofs are, of course, those from The Book. The PDFs, all typeset in the classic LaTeX font New Computer Modern, are accompanied by Lean code. Typically, such formalisations diverge from the formalisations in Mathlib: the contributors like formalising results ‘faithfully’, so the Lean code parallels the arguments from the books.

The repo Preliminaries contains the standard references for the field, covering the material undergraduates and PhD students are expected to master. It provides a shared language for mathematicians – human or AI. The first selection of texts was largely based on Reddit threads and Stack Exchange posts about reading recommendations, but the corpus was developed further with the help of world-class educators.

While the entire repo is available in printed form (five yellow books comprising 3,000 pages), it’s also available through a beautiful web interface with inline exercises. The world’s leading maths creators on YouTube were awarded grants to produce accompanying video lectures, while cognitive scientists received funding to incorporate mnemonic tools into the website. Today, most universities base their curriculum around Preliminaries, complementing the material with in-person lectures and collaborative problem solving sessions.

For many subjects, the standard references now also contain snippets of Lean code in theorem-like environments, prefaced by something like a bold-faced ‘Lean. 13.29’. These boxes have contributed to widespread Lean literacy: nowadays, every mathematician knows some Lean. Those inclined to formal mathematics view Preliminaries as human-readable Mathlib documentation, while inclined to informal mathematics view Mathlib as machine-readable Preliminaries documentation.

Beyond this, there are also repos with archives: proceedings from conferences, hand-written notes, video lectures – anything to give the AIs additional context, so they can place the exposition on the right level.

Another central repo is the list of open problems. In Open problems, humans and AI agents are welcome to submit solutions with autoformalisations as pull requests; a bot then checks that the Lean code compiles and agrees with the PDF writeup. If all checks pass, the problem is marked as solved and the associated files are channeled to Resolved problems. This repo is part noticeboard, part archive, and the most significant results, as judged by humans, get consolidated into the canon.

This rule, that only humans get to judge what goes into the canon, is seen as non-negotiable. While they don’t say so explicitly, people think there needs to be some rule preventing humans from becoming completely redundant. They can no longer deny that most mathematical output comes from AI agents: 87% of contributors are AI agents, and 96% of all novel results (theorems, propositions, lemmas) get solved autonomously by AIs.

The researchers #

What drives mathematical progress is no longer coffee beans, but tokens. Sometimes humans claim to figure out things ‘on their own’, whatever that means – everyone knows everyone else uses AIs, so naming theorems these days is considered anachronistic. But most people are transparent about their AI usage, and acknowledge that AIs now surpass human mathematicians in all dimensions.

It began as AIs became better at literature search. While they’d always had the ability to scour the entire internet, they usually kept on hallucinating references until the fall of 2025. However, in October 2025, AIs started pulling out solutions to open problems from prior literature. As they became better reliable search engines, they began drawing connections between different fields.

The same year, they became superhuman problem solvers. AIs already demonstrated strong problem solving skills in July 2025, achieving gold-medal standards at the IMO (this time, contrary to the year prior, they were well within the 4.5h time limit and could rely on informal reasoning). Then, in December 2025, they ranked among the top 3 of 4329 participants in the Putnam Competition. With continued increases in context window length, AIs soon acquired expert-level research taste, including the ability to articulate good research questions.

Heated debates about the role of the mathematician followed – it was as if AI developments unleashed an existential crisis among human mathematicians. In due time, experts stopped dismissing the progress in AI’s maths capabilities, especially after the breakthroughs on Erdős problem #1196 and the disproof of the unit distance conjecture.

In December of 2026, the International Mathematical Union conducted a study asking human experts to try distinguishing between human and AI-generated research questions. Humans and AIs were asked to generate ‘interesting’ questions centered around a class of papers the human knew well. The discrimination rate was 62%, hardly better than random guessing. The judges did, however, find the AI questions more compelling and worthy of study. And with that, the pipeline was complete.

Since AIs don’t need to eat or sleep, researchers began spinning up multiple research agents in parallel: one for crawling the internet and formulating research questions; one for trying to prove or disprove conjectures, piping its input back to the question agent; one for verifying arguments, both informally and formally; one agent for plotting and running numerics; another agent for presenting the results in a human-readable way. Naturally, all agents were built out of multiple subagents.

The presenter agent’s role has evolved rapidly. At first, it just tried producing lucid research monographs. This was easy: the raw mathematical output wasn’t too far from a research paper. Moreover, while superhuman, the AI agents had chains of thoughts resembling the way humans tackle problems. However, now presenters and human artists also experiment with other media to convey the mathematical content more efficiently. Sometimes, that’s just a PDF following the AMS Article format; sometimes, it’s an AI-curated website with interactive plots.

Researchers sometimes use presenter output for slow-paced recreational research, where the goal is to figure out a result together with AI. The fruits of the such research aren’t nearly as spectacular – the theorem statements are significantly weaker than those obtained by autonomous AI systems – but are more likely to go into the canon.

Early on, mathematicians agreed the canon shouldn’t contain anything a human mathematician cannot reasonably understand within their lifetime; some people jokingly speak of the problem complexity class ‘human lifetime’, and say it’s defined by the repo Canon.

Alongside recreational research, the new field of proof engineering focuses on pushing the boundaries of knowledge. The goals of this field include settling major open problems and verifying them in Lean, as quickly and flop-efficiently as possible. In practice, this involves the use of AI agents optimised for token efficiency and built to explore questions autonomously for longer periods of time. Without any optimisation pressure towards good exposition, they sometimes render intermediate results in Neuralese before stating their main results in natural language at the very end.

Resources have continued flowing towards this area. Being more resource-intensive, such mathematics is mainly conducted in AI labs. At first, some mathematicians criticised proof engineering for being a PR trick, diverting resources away from traditional mathematics. With time, however, proof engineering became seen as an integral part of mathematics.

So far, the efforts of the proof engineers have been fruitful. The AIs, instructed to stop only when arriving at an answer or proving that a solution is unattainable, successfully solved two millennium prize problems. Yang-Mills fell after seven months; for the Riemann hypothesis, AIs needed eighteen months of inference time. After that, for each problem, presenter agents spent an additional two months to distill the solutions into well-written textbooks. Considering the time these problems have remained open, these are still short timescales.

The experts who’ve started working through the textbooks sense that the theory is twice as deep as the theory required to prove Fermat’s last theorem. However, with Fermat’s last theorem, the proof served as a certificate that the problem was in the complexity class human lifetime. Mathematicians don’t know whether these solutions are within human lifetime. If they’re not, they won’t know it.

The humans #

Some humans like reviewing and redacting AI output, viewing it as their life’s mission to give AI-generated mathematics a human touch; they call themselves ‘Ourbaki’. To make the theory less daunting, the AIs usually incorporate intermediary results and real-world applications into their writeups.

For some reason, this kind of research appeals to the human mathematicians who used to be singularly focused on their own research before 2025. Others, demotivated by the feeling of not getting to do anything for themselves, turn to other careers.

Most academics focus on recreational research and teaching well, leaving proof discovery to the proof engineers. Since many old-school research mathematicians prioritised research over teaching, mathematicians today prefer the term ‘curating’. The curator’s goal isn’t just to teach – whether material from Canon, Preliminaries, or any engineered proofs – but also to instill a love for problem solving, and convey an appreciation of the results. In this respect, they’re much like their colleagues at the humanities departments.

Those doing slow mathematics – recreational researchers, Ourbaki and curators – are candid about their role in society. The main value of human-oriented mathematics, they say, doesn’t come from the applications; for applications, there are the applied sciences and proof engineering. Instead, the curators view their duty as building human capital and enriching the world’s cultural heritage. Over time, grantmakers have accepted this shift of tone in grant proposals.

Epilogue #

This is fiction, but it’s also bad fiction. I’ve tried keeping the narrative plausible and, to the extent possible, neutral. Whether and when such a scenario might occur is left as an exercise to the reader.

This post was largely inspired by the episode with 3b1b on the Dwarkesh podcast.