Within a decade or two, mathematics will probably 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. This will change the discipline.

Below is one way things could turn out. I’ll leave you to judge the probability of the scenario – it’s a dinner table kind of discussion.

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 between community members in coffee breaks at conferences. Even a relatively niche field like algebraic K-theory can’t feasibly invite all world-leading contributors: once the digitalisation of mathematics became cheap and scalable, with autoformalisation agents writing Lean code up to MathLib standards, mathematical research communities grew to encompass thousands of members. This has led to unprecedented progress: people with no formal background in mathematics have made significant contributions, 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 exquisite new computer modern, are accompanied by self-contained Lean code. The contributors typically challenge themselves to formalise results ‘faithfully’, so the Lean code parallels the arguments from the books.

The repo Preliminaries contains the standard references for the material undergraduates and PhD students should master, providing a shared language for mathematicians – human or AI. The first selection of texts was largely based on Reddit threads and StackExchange posts about reading recommendations, but the corpus was developed further with the help of expert 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. Grant Sanderson was awarded a grant to produce accompanying video lectures, while Andy Matuschak and Michael Nielsen were charged with incorporating mnemonic tools into the website. Anyone working through the website – doing all the exercises and flashcards tailored to that user’s level – was bound to learn something. 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 a bold-faced ‘Lean. 1.23’. Since such boxes also point to explicit parts of MathLib, some people scorningly call the repo Mathlib 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.

Most of the mathematical output comes from the AI agents: 70% of contributors are AI agents, and 97% 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.

First, 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. It was like AIs had broader knowledge than people like Henri Poincaré or Jean-Pierre Serre, widely regarded as the last human generalists.

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.

Debates about the role of the mathematician followed. Human 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 late 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 so-called recreational research, where the goal is to figure out a result together with AI. The fruits of human-oriented 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.

A new field called proof engineering focuses on pushing the boundaries of knowledge. The goals of this field include settling major open problems and verifying them in Lean, using as few flops 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. Some mathematicians criticise proof engineering for being a moonshot endeavour, diverting resources away from the traditional kind of mathematics. However, the efforts 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 FLT, 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. To make their theory less daunting, the AIs usually weave in intermediary results and applications. The human mathematicians singularly focused on doing cutting-edge research before 2025 usually take on this kind of role, and they dub this research programme ‘Ourbaki’.

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 help others appreciate the theory. In this respect, they’re much like their colleagues at the humanities department.

The curators are candid about their role in society. The primary value of human-oriented mathematics, they say, doesn’t stem from the applications; for applications, there are the applied sciences and proof engineering. Instead, the curators view their duty as building human capital and contributing to human culture. Over time, grantmakers have accepted this shift of tone in grant proposals.

Epilogue #

This narrative is meant to be plausible – I’m no big fan of sci-fi, but using the conditional everywhere in the was inconvenient. To the extent possible, I’ve tried keeping the narrative neutral.

Whether and when such a scenario might occur is left as an exercise to the reader.