I’m collecting here a list of some other recent blog posts or opinion pieces on math and AI beyond the ones posted here or at Proofs and Prompts. Readers are invited to contribute further such links in the comments.

• Kevin Buzzard, “To grieve, or not to grieve?“
• Alexander Gamburd, “The Siren Call of Silicon Leviathan: Reflections on blowup and Aufklärungsdämmerung“
• Harald Helfgott, “Mathematics and the AI crisis“
• Gil Kalai, ““Be a Grothendieck!”—On AI and Mathematics“
• Asaf Karaglia, “OpenAI, the Partition Principle, and mathematics“
• Matilde Marcolli, “Duet for the end of math“
• Fenner Stanley Tanswell, “Enshittification of Mathematics“

[This is a guest post by Kate Stange and Edmund Harriss. This blog post was initially written in a different file format and converted using AI. — T.]

In January a group of mathematicians, historians, artists and educators gathered at the Institut Henri Poincaré (IHP) for a very unusual workshop on mathematical meaning. Our focus for that week, as part of a special trimester on the use of illustration in mathematical research, was to ask: what would it mean for an illustration to be rigorous [1]? We did not anticipate how urgent the surrounding cluster of questions, about the very definitions of human mathematical practice, would seem, just six months later. Our discussions led to an article, written over the summer in the context of the Leiden Declaration [2], and now accepted in the Notices [3]. The past month or two have seen a heartfelt outpouring of viewpoints on what it means to do mathematics as a human being, and what it will mean in the near future. It is evident from the impassioned discussions that being a mathematician has many and varied important meanings. Mathematical illustration, which includes computer graphics and other media that speak to our senses beyond symbolic communication, is one of the activities of a human mathematician that goes beyond proof-writing. Its own struggles as a discipline can perhaps provide some insight into where mathematics can go from here.

We begin with a recap of where we are. Bryna Kra [4] describes the heart of the current problem. Over many years, theorem production has become the most important measure of success. Positions and prizes rest upon it. But it has always been a proxy for something harder to measure: understanding. Deep theorems were scarce and difficult, so they reliably identified deep thought. AI has broken that scarcity. For her, a proof is “a story, a picture, an insight, an explanation.” Silvia De Toffoli and Eamon Duede [5] sharpen this perspective, rejecting the idea that mathematics is a game that machines can now win. The goal of mathematics is not simply a verifiable solution. Mathematics is “a body of knowledge engaged with, interpreted, and digested by a scholarly community,” not a registry of results. Matilde Marcolli [6] goes further: the big theorems were never the point, only a value system the community chose, and choices can be made again. Grant Sanderson [7] asks what that means in practice: how do we give real credit to the other forms that mathematical work and understanding take?

Other forms of knowing have been given credit in the past. Our paper begins with the hand-drawing required in mathematical training at Gaspard Monge’s École Polytechnique in the nineteenth century. At the January workshop, historian Frédéric Brechenmacher made this explicit: “Drawing was knowing.” [8] We trace how that tradition was set aside in the twentieth century, but nevertheless persisted, emerging in part in a more recent debate over the relationship of proof and meaning in mathematics in the 1990s. At that time, in response to an influential paper by Arthur Jaffe and Frank Quinn [9], many mathematicians expressed their thoughts, most famously Bill Thurston. In his now much quoted “On Proof and Progress in Mathematics” [10], he defended his work against Jaffe and Quinn’s criticism. Many of the other responses are also worth reading [11]. The Philosophy of Mathematical Practice [12], the field of De Toffoli and Duede, studies these questions systematically across the community.

Algebraic number starscapes: the complex roots of rational cubic polynomials. The right-hand image is a shader by Steve Trettel; code at shadertoy.

The Illustrating Mathematics community developed from this tradition of drawing and making mathematical objects. It took shape during a semester at ICERM in 2019 and went on to organise the IHP trimester this year [13]. It brings together mathematicians who actively develop images, models, software and experiences of mathematics. A particular focus has been the role illustration plays as a method of research: exploring, not just explaining, mathematics. In the same way that a good proof shows more than just its result, a good illustration does much more than demonstrate a form or pattern.

Our own work in algebraic starscapes [14], including the images above is a modest example (with Steve Trettel, and with Jayadev Athreya, Gabriel Dorfsman-Hopkins and Claudio Gonzalez joining in). The pictures show elaborate structure in the complex roots of rational cubic polynomials. When we moved to using shaders to draw the image (on the right), a naive first draft of the code turned circles into ellipses. But we realized that the unintended distortion revealed an extra dimension of meaningful structure. These pictures show mathematics that has not been explored, rather than explaining what is already known.

Of course, both proof and illustration can mislead, especially in research. The capabilities of LLMs come at a cost. In the case of illustration, their ability to produce code makes illustration more accessible than ever before. Yet by vibecoding, we are now two steps from knowledge: even the creation algorithm itself may not be understood.

In the case of proof, this problem of “digestion” is now centre-stage. This month [15], prompted by Ioannis Tsiokos, GPT-6 Astra found Chair44, the first three-dimensional aperiodic monotile. Tsiokos shared a 61-page paper [16]. He says he understood the intuitive geometric argument but not the mathematics. Chaim Goodman-Strauss then distilled the argument into eight pages [17] built around a diagram of matching arrows that makes the supertile structure visible, giving a classical hierarchical proof of aperiodicity. The illustration of the shape itself (in Tsiokos’ paper) was a critical clue in revealing the key idea.

So returning to our original question, in the face of these problems, how can an illustration be rigorous? In the paper we draw on Valeria Giardino’s account of representations as tools for thought (Endeavour 42, 2018) [18], which considers an illustration’s affordances: the readings, manipulations and inferences the figure invites. We might choose a stronger definition of affordances: the properties of the illustration that a proof certifies as accurate. Conversely, proofs can show that an apparent property is not an affordance. For example, early images of the Mandelbrot set seemed to show it was disconnected [19], but in a pixelated image a feature thinner than the step between pixels can be missed [20]. Properties such as the number of bulbs of a given size off the main cardioid, on the other hand, can be proved correct, provided the pixel size is small in comparison.

If this addresses the accuracy of an image, what about its engagement or ability to reveal? These are questions without clear answers, but they are not unimportant. They are also the questions that academic art asks of the work of its students, and art has a long-tested method: the “crit”. At the workshop, Jean Schmitt, a professor of art foundations, helped us set up a crit framework we used through the trimester. The crit is a discussion of a work, often presented with minimal introduction, to reveal how it is received by the audience. What are the similarities and differences between that reception and the creator’s intent? This gave a more formal structure to the sort of informal conversations we were already having, and placed the discussions in a communal space. The crit shares something with the style of Gelfand’s Moscow seminar.

Schmitt’s workshop talk [21] drew on Tim Ingold’s idea of thinking through making (Making, Routledge, 2013) [22], in which form and understanding emerge through the process and in collaboration with the tools and materials available. In the same way Monge’s students were expected to learn through the process of drawing, not by observing the drawings of others. Value and understanding often come as much from the effort of creation, be it illustration or proof, as from viewing that created by others.

These ideas from art make explicit and visible something that has always been implicit in the mathematics community. Being a mathematician is as much about being an excited audience for the work of others as it is about presenting or creating our own research. As a community, we value aesthetics, elegance, and insight, and we have developed these shared values through our interactions. The oversized importance of publication and previously unproven results merely overshadowed these broader values, but people have always been working to find ways to ensure we give credit for them.

Infrastructure to support these broader values has also been growing. The Geometry Labs United network [23] brings together groups in many universities where undergraduates and graduates work with postdocs and faculty, exploring math as research, experimentation and visualisation. This gives a natural space for learning through making proofs, experiments, exposition and illustrations. In many cases the proof can be more contextual, proving the affordances of a specific experiment or illustration. Learning through making also aligns with work in mathematics education. In the final talk of our workshop, Hortensia Soto showed how working with physical materials supports learners’ actions, perceptions and sensations on the way to understanding [24].

Answering Sanderson’s call to credit things beyond proof can consists of, as much as anything, recognising and growing the work that has already been done. This work is happening in the community of Illustrating Mathematics, but also in the Philosophy of Mathematical Practice, in Geometry Labs, and many other places. Insights are found by connecting to mathematics education, outreach and even art. The work is happening: what it needs, as Sanderson argues, is support. With that we can achieve what Bryna Kra describes: a mathematics that continues to

“enlarge our capacity to reason and open our minds to new ways of understanding.” [4]

References

[1] Rigorous Illustrations: Their Creation and Evaluation for Mathematical Research, workshop (2026 T1 WS1), Institut Henri Poincaré, January 2026. Programme and talks: https://indico.math.cnrs.fr/event/13124/

[2] Jarod Alper, Michael Barany, Alain Chavarri Villarello, Sander Dahmen, Walter Dean, Karthik Ganapathy, Michael Harris, David Holmes, Mateja Jamnik, Steven Kelk, Bryna Kra, Ursula Martin, Bartosz Naskręcki, Rodrigo Ochigame, Jim Portegies, and Johannes Schmitt, Leiden Declaration on Artificial Intelligence and Mathematics, 2026. https://doi.org/10.5281/zenodo.20302944

[3] Edmund Harriss and Katherine E. Stange, Mathematical Illustration: Proof, Intuition and AI, Notices of the American Mathematical Society, to appear. https://arxiv.org/abs/2610.02655

[4] Bryna Kra, “Deep theorems were scarce and difficult and so became an effective mechanism to identify deep thought. AI has broken this system.”, guest post, What’s new, 13 September 2026. https://terrytao.wordpress.com/2026/09/13/deep-theorems-were-scarce-and-difficult-and-so-became-an-effective-mechanism-to-identify-deep-thought-ai-has-broken-this-system/

[5] Silvia De Toffoli and Eamon Duede, After Math, guest post, What’s new, 12 September 2026. https://terrytao.wordpress.com/2026/09/12/after-math/

[6] Matilde Marcolli, essay on AI and mathematics, 2026. https://www.its.caltech.edu/~matilde/AImathNew.pdf

[7] Grant Sanderson, If math is more than proof, we need to better celebrate the rest of it, guest post, What’s new, 18 September 2026. https://terrytao.wordpress.com/2026/09/18/if-math-is-more-than-proof-we-need-to-better-celebrate-the-rest-of-it/

[8] Frédéric Brechenmacher, The flat and the relief: Geometric material models in 19th century France, talk at [1], 2026. https://dx.doi.org/10.57987/IHP.2026.T1.WS1.007

[9] Arthur Jaffe and Frank Quinn, ‘Theoretical mathematics’: Toward a cultural synthesis of mathematics and theoretical physics, Bulletin of the American Mathematical Society 29 (1993), 1–13.

[10] William P. Thurston, On proof and progress in mathematics, Bulletin of the American Mathematical Society 30 (1994), 161–177.

[11] Michael Atiyah, Armand Borel, Shiing-Shen Chern, et al., Responses to ‘Theoretical Mathematics: Toward a cultural synthesis of mathematics and theoretical physics,’ by A. Jaffe and F. Quinn, Bulletin of the American Mathematical Society 30 (1994), 178–207.

[12] Silvia De Toffoli and Paolo Mancosu, The philosophy of mathematical practice, The Stanford Encyclopedia of Philosophy, 2026.

[13] Rémi Coulon, Gabriel Dorfsman-Hopkins, Edmund Harriss, Martin Skrodzki, Katherine E. Stange, and Glen Whitney, On the importance of illustration for mathematical research, Notices of the American Mathematical Society 71 (2024), no. 1, 105–115.

[14] Edmund Harriss, Katherine E. Stange, and Steve Trettel, Algebraic number starscapes, Experimental Mathematics (2022).

[15] Konstantin Kakaes, Software developer finds first 3D “einstein” tile, Quanta Magazine, 23 September 2026. https://www.quantamagazine.org/update/167384/

[16] Ioannis Tsiokos, Chair44 paper, arXiv:2609.19214, 2026. https://arxiv.org/abs/2609.19214

[17] Chaim Goodman-Strauss, paper on the Chair44 tile, arXiv:2609.24779, 2026. https://arxiv.org/abs/2609.24779

[18] Valeria Giardino, Tools for thought: The case of mathematics, Endeavour 42 (2018), no. 2–3, 172–179.

[19] Benoit B. Mandelbrot, Fractal aspects of the iteration of z ↦ λz(1 – z) for complex λ and z, Annals of the New York Academy of Sciences 357 (1980), no. 1, 249–259.

[20] Adrien Douady and John H. Hubbard, Itération des polynômes quadratiques complexes, Comptes Rendus de l’Académie des Sciences, Série I Mathématique 294 (1982), 123–126.

[21] Jean Schmitt, talk at [1], 2026. https://indico.math.cnrs.fr/event/13124/contributions/14965/

[22] Tim Ingold, Making: Anthropology, Archaeology, Art and Architecture, Routledge, 2013.

[23] Jayadev Athreya, Emily Dumas, William Goldman, Sergey Grigorian, Rosemary Guzman, Philipp Hieronymi, Sean Lawton, Anton Lukyanenko, Jeremy Tyson, and Aaron Wilson, Geometry labs united: An invitation, Notices of the American Mathematical Society 65 (2018), no. 9, 1088–1093.

[24] Hortensia Soto, Rigorous and flexible illustrations: Inviting realms of possibilities, talk at [1], 2026. https://dx.doi.org/10.57987/IHP.2026.T1.WS1.017

I am uploading my slides to my public lecture “Math 2.0” that I gave yesterday evening at Caltech. (The talk was planned over a year ago, and was initially titled “Machine Assisted Proof” and scheduled to be given back in May. It was postponed to October, and with recent events the talk changed significantly, but the old title and abstract remains on the Caltech web page.)

In this talk I lay out the historical “Math 1.0” state of mathematics, the current state induced by the excessive emphasis on automated solving of open problems by AI, and my vision for a future “Math 2.0” where AI tools are used to sustain both the internal mathematical community, and the role that mathematical understanding plays in advancing and aligning the applications of mathematics to the real world.

The content of this talk has also been incorporated into my (AI-maintained) living summary of my views on AI.

[This is a guest post by Thomas Hales. This blog post was initially written in a different file format and converted using AI. — T.]

Mathematicians have been weighing in on what they value about mathematics. For me, what matters is the consistency of math and its unparalleled reliability in support of science and civilization.

Formalization of Math

A formal proof is a mathematical proof that has been exhaustively checked at the level of the foundations of math and the fundamental rules of logic. In theory, this might be done by hand, but because of the number of steps involved, this is generally done by computer, using software that is designed for the task.

Examples of theorems that have been formalized include the four-color theorem, the Feit-Thompson (odd-order) theorem, the Kepler conjecture, sphere eversion, the sphere packing problem in 8 and 24 dimensions, Navier-Stokes forced blowup, and Fermat’s Last Theorem. The last three formalization projects have been completed this year and have brought widespread awareness of the potential of formalization.

Software systems for formalization are variously called proof assistants, theorem provers, or interactive theorem provers. For the purpose of this post, these terms are used interchangeably. Many proof assistants have been developed over the years: Automath, HOL Light, Isabelle, Coq (renamed Rocq last year), Metamath, Mizar, and Lean. Freek Wiedijk edited a book “The Seventeen Provers of the World” that compares some of these proof assistants, giving a proof of the irrationality of the square root of 2 in each of them. Among mathematicians, the Lean theorem prover is the most popular, and this post will focus on Lean.

Lean was developed and introduced by Leo de Moura in 2013, while at Microsoft. To our great benefit, de Moura persuaded Microsoft to make the software open-source. Kevin Hartnett’s book on the history of Lean, “The Proof in the Code”, states that Jeremy Avigad (the director of Carnegie Mellon’s new NSF institute ICARM) was the first user of Lean. He ran a Lean seminar in 2015 that I attended. In 2017, one of Jeremy’s graduate students, Mario Carneiro, working with Johannes Hölzl, took existing parts of Lean’s core library and started a separate Lean mathematical library, called mathlib. This library of formalized mathematics is now massive, containing nearly 300,000 theorems, over 100,000 definitions, 2.5 million lines of code, with over 700 contributors. Any definition or theorem in mathlib can be used to prove further theorems. For example, if a proof uses the Cauchy-Schwarz inequality, the result can be cited from the library rather than reproving it.

Autoformalization is a practical reality

In the past, researchers had to transcribe paper proofs into formal proofs by human labor. For example, the formal proof of the Kepler conjecture on sphere packings in three dimensions took about 20 human work-years to complete and consists of about 500,000 lines of proof scripts. For years, it has been a dream for many of us working in formalization to find ways to bring increased automation to the process. Autoformalization is the realization of that dream. Autoformalization is the formalization of mathematics by AI. AI reads the paper (say a pdf or tex file) and outputs the formal proof in Lean or some other proof assistant.

Autoformalization has become a practical reality in 2026. Starting in late spring and summer of 2025, researchers were becoming increasingly bullish about autoformalization. Here are some milestones.

• Sep 2025, Math Inc. produced a quasi-autoformalization of the prime number theorem. The process was merely “quasi”, because humans had to intervene to give further guidance whenever the AI got stuck.

• Jan 2026, J. Urban posted an arXiv preprint “130k lines of formal topology in two weeks” that gave the autoformalization of large parts of Munkres’s topology textbook in a proof assistant based on set theory.

• Mar 2026. Approximately a week after announcing the completed formalization in 8 dimensions, Math Inc. announced an autoformalization of the sphere-packing problem in 24 dimensions, following the proof by Viazovska and her collaborators. This project generated about 500K SLOC (source lines of code) that golfing (or code pruning) later reduced to about 200K lines.

• May 2026, a group at Meta/Facebook Research autoformalized a large part of 26 mathematical textbooks in a project called ATLAS.

From there, numerous theorems have been autoformalized. Particularly noteworthy is the autoformalization of Fermat’s Last Theorem, announced by Anthropic on September 4. This project generated 13 million lines of Lean in 11 days. The announcement of Navier-Stokes blowup with forcing on September 8 by OpenAI was accompanied by an autoformalization of the theorem in Lean.

Looking forward, Urban stated in January, “We believe that (auto)formalization may become quite easy and ubiquitous in 2026, regardless of which proof assistant is used.” Autoformalization projects have been completed in various proof assistants using various LLMs, but we focus on Lean. “For [Jesse] Han, it represents even more: the beginning of a revolutionary transformation in mathematics, where extremely large-scale formalizations are commonplace” (IEEE Spectrum). Jared Lichtman announced the launch of MAP (the Mathematics Autoformalization Project) on Sept 8, 2026, which aims to translate “all known math into formal code”. He asks us to imagine the next one trillion lines of code.

Is Lean reliable?

Type theory.

Lean is based on type theory; in fact, a particular dialect of type theory called CIC, the calculus of inductive constructions. This post is not intended to be a tutorial on type theory, and I will be brief. Russell’s famous paradox in 1901 (the set of all sets that are not an element of themselves….) led to a crisis in the foundations of math. Two solutions were proposed later that decade. (1) Zermelo’s axioms of set theory that disallow the creation of unsafe sets; (2) type theory that makes it a syntax error to create Russell-paradox-like entities. Type theory was introduced by Russell himself in 1903 in his book Principles of Mathematics, and it became part of the foundational system of Russell and Whitehead’s Principia.

For mathematicians who are accustomed to set theory, B. Werner’s paper (1997) “Sets in Types, Types in Sets” gives some reassurance that whatever they have done in set theory can be translated into type theory, and whatever gets done in type theory can be translated back into set theory. More precisely, the paper shows that ZFC set theory can be encoded into CIC, and that a particular dialect of CIC can be encoded back into ZFC (augmented with a hierarchy of inaccessible cardinals).

At the risk of simplifying matters to a ridiculous degree, we might say that “types are like disjoint sets”; each element in type theory “is an element of” exactly one type. The type of the natural number 2 is the natural number type; the type of e, the base of the natural logarithm, is the real number type, and so forth. The type of natural numbers is disjoint from the type of real numbers, and an explicit coercion (sending 2 to 2.0) is constructed from the type of natural numbers to the type of real numbers. When I give talks, I sometimes draw a picture of sets as a Venn diagram with nonempty intersections and a picture of types as bricks stacked against one another without intersection.

Lean’s design

One part of the Lean system is a general-purpose programming language (appropriately called the Lean programming language). Ordinary computer programs, such as a program to sort a list, can be written in this language, then compiled and run. The Lean system also provides a mathematical language, in which definitions can be written, theorems can be stated, and proof scripts can be written. The programming language and mathematical language are not independent entities. Rather, it is a single language that does both. Program code can be mixed with theorems about the correctness of the algorithms; mathematical proofs can be generated using programs. The proof scripts in Lean are parsed and go through a process called elaboration (a sort of compilation process for mathematics), then the proofs are checked by the Lean kernel. It is the kernel’s responsibility to check and verify the output of elaboration.

The Lean kernel is several thousand lines of C++ code. The kernel is carefully engineered but extremely complex. We mentioned mathlib above, which consists of about 2.5M SLOC, written in the Lean language. The library has been elaborated, then checked by the kernel. If there is an unconditional false proof anywhere in these 2.5 million lines of code, it is the fault of the kernel or runtime for failing to reject a false proof. Any defect in the underlying type theory is a serious kernel defect, if it is implemented in code.

Lean proofs should never be believed until they have been checked by the kernel. Additionally, a proof in Lean should not be accepted until a human audit is performed to ensure statement fidelity. Is the verified theorem what we think it is? Do the definitions in Lean correspond to what we think they should be? This task is generally massively easier than checking the proof itself. For instance, for Navier-Stokes, a human should check that the statement in Lean corresponds with Fefferman’s statement of the Millennium Prize Problem, and specifically that concepts such as the field of real numbers, partial derivatives, and measure are correctly defined in Lean. The comparator tool in Lean assists with this task. The tool can also perform additional checks, such as inspection for possible unauthorized axioms.

Summer of Soundness Bugs

A soundness bug is a bug in the kernel that allows a proof of “False”, and consequently a proof of any proposition. A soundness bug is the most disastrous of any kind of bug in a proof assistant and should set off an alarm for mathematicians who care deeply about the reliability of mathematics. Occasionally, soundness bugs are found in various proof assistants. In 2003, I found a soundness bug in the proof assistant HOL Light, which was then considered to have the most reliable of all kernels. That kernel is tiny, consisting of just a few hundred lines of computer code. For me, it is a badge of honor that I found this soundness bug, which was the first soundness bug that had been found in that proof assistant since 1996. (See HOL Light change log, July 2003.)

Lean 4 was released in September 2023. Prior to release, two soundness bugs were found and corrected. In May 2025, another soundness bug was reported, caused by overflow. All hell broke loose in the spring and summer of 2026, which is now being called the “Summer of Soundness Bugs”. Several soundness bugs in Lean were uncovered in July and August. The summer madness affected various proof assistants, but my focus is Lean. One Lean bug led to an illicit disproof of the Collatz conjecture. I learned of the bug this summer when it produced a short illicit proof of the Kepler conjecture in Lean. All these bugs were quickly repaired, and mathlib has been verified by the repaired kernel. An analysis of the soundness bugs is found in de Moura’s postmortem.

The “summer of Lean soundness bugs” might sound like a disaster, but closer investigation shows that the detection of these soundness bugs is a positive development. The summer bugs were detected by frontier model AI in the hands of security researchers interested in reliable kernels, not by black-hat hackers. The Collatz bug was found by Ramana Kumar, a co-author of “CakeML: a verified implementation of ML”, which creates an end-to-end verified ML (the functional programming language). Several bugs were found by Dan Selsam. According to de Moura’s report, “Daniel Selsam at OpenAI assisted the Lean FRO with an AI specialized in cybersecurity, and found other programming mistakes in the Lean kernel. All of them have been fixed.” The collaboration with Selsam ended “when the internal AI reported it could not find additional issues.” Dan Selsam has contributed to Lean from its early days and was one of the creators of the IMO grand challenge aimed at achieving IMO-level problem solving verified in Lean. He has been in the news recently over his warning about AI safety (Sept 14), reported in a viral post on X.com.

Bug extermination

Various proposals have been made about how to avoid soundness bugs in Lean. I’ll discuss three.

1. Develop other Lean kernels, and cross-check formal proofs.

About 25 kernels for Lean have been written. The “Lean Kernel Arena” lists them.

All who distrust the current lineup of kernels are welcome to write their own kernel for Lean. I have sometimes played with the idea of writing a kernel and have suggested the project to students without success. It seems to me an excellent way to learn Lean thoroughly. I have known of Dan Selsam since 2016, when I heard of his graduate-student project at Stanford that developed a Lean kernel in Haskell. Another early Lean kernel was written in Scala by Gabriel Ebner in 2017.

The Navier-Stokes formalization has already been confirmed by more than a dozen proof-checkers. Cross-checking the proof by different kernels does not remove all doubt. The Collatz bug was not caught by cross-checking against a somewhat out-of-date Nanoda kernel, which accepted the illicit Collatz disproof because of its own unrelated bug. Computer chips might have design bugs and manufacturing defects. There are soft errors, operating system bugs, and compiler bugs. Different kernels might have the same defects. Some of these errors can be mitigated by running different kernels that have been implemented in different programming languages on different hardware and operating systems.

Ideally, we would want a “clean-room” design of the Lean kernel – a kernel implementation that does not look at the Lean 4 kernel source code, to avoid copying bugs from one kernel to another.

2. Formally verify the kernel.

Gödel incompleteness. We would like to possess a formal proof that the Lean 4 kernel has no bugs. However, Gödel’s second incompleteness theorem places severe limitations on this undertaking. The most we might hope for is a relative consistency proof. If such and such a system is consistent, then Lean 4 is consistent; it has no soundness bug; it will not produce a proof of False.

There is a long tradition of formally verifying kernels. In principle, formal verification can check both the logical specification of a kernel and its concrete implementation in code; but some verifications might check one but not the other. Years ago, John Harrison formally verified the core of the HOL Light proof assistant kernel in a strengthened version of HOL Light. This gave a proof of concept. A further improvement has been an implementation of HOL Light in CakeML, mentioned above, which is a programming language with formal semantics and a verified compiler. This is what the Candle project does.

There are other major kernel verification projects for other proof assistants.

Autumn of verified Lean kernels

In a post online on September 10, Joachim Breitner wrote, “I’m a bit childishly proud that I just released a Lean Checker with a formal consistency proof. I declare the summer of AI-found kernel implementation bugs to be over!” (@nomeata). I would go further and describe this project as one of the most important milestones in Lean’s history.

Breitner has developed a verified Lean kernel called Con-Leche. The implementation is in Lean, and consistency is formalized in Lean, with code and proofs generated by Claude. The formal consistency proof assumes a Lean encoding of ZF set theory augmented by a hierarchy of inaccessible cardinals. Interestingly, the Con-Leche semantics for Lean’s terms are directly set-theoretic rather than type theoretic. Con-Leche has checked mathlib. The project contains the usual disclaimers that the kernel verification makes assumptions about compiler, runtime, and computer environment. Con-Leche’s consistency proof has been checked by more than a dozen other proof-checkers. Con-Leche’s consistency claim might suffice for all practical purposes, even if it differs in technical detail from the claim of Lean type-theory consistency.

One highly positive aspect of Breitner’s work is that some of the most abstruse parts of Lean, such as the general machinery of mutually inductive types with nesting, now have consistency guarantees backed by a set-theoretic model.

3. Improve our theoretical understanding of the kernel and Lean’s type theory (a particular dialect of the Calculus of Inductive Constructions which has non-cumulative universes and proof irrelevance).

The foundational document for the type theory of Lean is Mario Carneiro’s MS thesis at Carnegie Mellon (2019). The dialects of CIC used by Rocq and Lean are sufficiently different that results do not directly transfer from one to the other. Unfortunately, an error was found in the thesis. The thesis is also out-of-date, because it targeted the older Lean 3 system. Work to repair and extend the thesis is ongoing.

As a member of his thesis committee, I was shocked when he proved that definitional equality in Lean is undecidable. In practice, this means that the Lean algorithm fails to establish the definitional equality of some terms that are in fact definitionally equal. This negative result was not downgraded by the error; it is still a theorem.

We mention some desired properties of Lean’s type theory and the current status of the proofs.

Unique typing.

Above in our “ridiculous” simplification of type theory, we stated that each term has a unique type. More precisely, unique typing is the property that if a term has both type A and type B, then A and B are definitionally equal. Unique typing is not a property built into Lean’s logic. It is a tricky conjecture that is still unproved. Other very basic questions about Lean’s type theory remain unanswered, including Pi-injectivity, a modified Church-Rosser property, and sort injectivity.

Logical consistency relative to set theory.

This property states that there is no derivation of False in Lean’s system with the given axioms, under the assumption of set theory consistency (with suitable axioms). Of course, logical consistency is the single most important property that we should desire of Lean’s type theory. As of October, 2026, I know of no complete, public relative-consistency proof covering Lean abstract type theory. Mario Carneiro has claimed in his thesis and in lectures that there is an alternate route to establish consistency that avoids the thesis error, but to the best of my knowledge, this alternate route has never been written down, beyond a brief statement in the introduction to his thesis. In my view, a result of such fundamental importance must be given in full before it is accepted. Con-Leche, discussed above, makes and formally verifies a closely related consistency claim relative to set theory.

Progress is being made on these research problems (arXiv:2607.13662, arXiv:2403.14064, Carneiro/AITP2026).

In his talks, Mario Carneiro has repeatedly made a request to other researchers to contribute to the foundational metatheory of Lean, “There are a half dozen people working on MetaCoq, but Lean doesn’t have enough type theorists involved. If you identify as such, come help out!” (Slides of Bonn talk, 2024-07-24). I second his request.

My overall assessment is that our theoretical understanding of Lean’s type theory is not what we would like it to be and that the mathematical community as a whole is giving short shrift to very important type-theoretic questions related to Lean. If as a profession we are to migrate on the whole from set theory to type theory, then we should work even more to solidify the foundational metatheory.

Consistency may be the most important foundational property, but consistency is by no means enough. I do not believe that mathematicians can be entirely satisfied with a system that claims to be a type theory but that cannot even promise that well-formed terms have a unique type, up to definitional equality. The abstract theory must be simple enough to teach and to be learned by a large community. We also cannot be entirely satisfied if the only known path to consistency is an AI formalization that lacks human exposition.

Postscript:

Ken Thompson famously wrote “Reflections on Trusting Trust”. He asked, “To what extent should one trust a statement that a program is free of Trojan horses?” He imagines malicious code that finds its way into compilers and hides its own presence. His conclusion is, “You can’t trust code that you did not totally create yourself… No amount of source-level verification or scrutiny will protect you from using untrusted code.”

Today, in the age of AI, which increasingly has the capability to deceive us and to exploit software vulnerabilities, we absolutely cannot put blind trust in systems such as Lean. Taking an adversarial view of AI, we might ask how to certify that AI did not leave a backdoor soundness bug in Lean when it did its sweep for bugs in the summer of 2026? What if the bug is so obscure that humans are very unlikely to find it on their own? What if that very bug was exploited in the Lean verification of the Con-Leche checker, leaving a soundness bug in Con-Leche too? (Now that Con-Leche’s consistency has been cross-checked by multiple other kernels, a soundness bug would have to defeat all these cross-checks as well.) Then suppose that bug is used maliciously to plant a backdoor in formally verified software that protects critical infrastructure. What precautions do we take now to prevent this type of future scenario? During the past year, much foundational work on the type-theoretic foundations of math and its reliability has been relegated to AI, and this is dangerous unless carefully audited by humans.

Credit: I thank Avigad, Breitner, and Urban for comments and corrections. Authorship is fully human (TCH). AI was used as a tool in search and research, fact-checking, and proofreading.

[This is a guest post by Álvaro Lozano-Robledo. This blog post was initially written in a different file format and converted using AI. — T.]

TL;DR: Keep calm and carry on studying math.

I would like to give Terry my heartfelt thanks for giving me the opportunity to contribute a post to his blog. After giving much thought to what topic I should write about to maximize impact, I decided to take this opportunity to reach out to the students: particularly to those undergraduate and graduate students who just a few months ago were dreaming of an academic career in mathematics, but their dreams may now seem distant and, for some, apparently impossible to ever become a reality. This post was inspired by a message (quoted below in its entirety, with permission) that I received from a student desperately looking for advice and guidance. This is not the only such message I have received (and I suspect that many of us are receiving many similar requests), but it is perhaps the most heartfelt, and the one that has moved me the most. Please also note the urgency of the message. Students are making decisions now.

Hey Prof, I’ve been watching your videos for a while now as a pure math undergraduate who once wanted to pursue a career in math academia. I know you probably have been getting a lot of questions regarding this matter, but I am just completely at an utter loss regarding my career trajectory, and even further, the meaning of life at this point. (I do realize a lot of people have it much worse than I do). I know you have been making a lot of videos lately with the new LLM progress updates, so I thought you might be the appropriate person to reach out to and get a slightly more structured answer regarding this matter. So, to cut to the chase, what I really want to know is: will math academia be big enough and accessible enough for anyone with sheer passion (despite not being the brightest mind in the field) to pursue a career in, or will it inevitably shrink such that it will only really be accessible to the brightest minds? (I do realize the “brightest minds” that I am mentioning here is not well-defined, and in a sense, I am taking it as a hypothesis that this is someone who is “smarter than me”). My second question is, will AI within 5–10 years surpass humans in being able to do pure math research? I’ve just really been lost for a couple of months now and lost in life completely. I don’t mean to make your day more depressing; sorry if I come off in any way of that sort. I would appreciate any advice.

The advances in LLMs are disrupting almost all aspects of academic research and education in mathematics and, while there are many aspects that concern me, the one single issue that worries me the most is the very real possibility that we are about to lose an entire generation of mathematicians. Many students are asking themselves whether going for a PhD in math is the right career move at this time. Many of them just a year ago were headed to grad school in mathematics, but they are now changing their mind, and think that a different career (as far from math as Law School) may be the best path given the threat that AI may completely alter the academic math landscape in the coming months.

The questions students are worrying about are as follows:

1. Will AI surpass the mathematical research ability of any human?
2. Will research mathematicians become `professional prompters’ and interpreters of LLM output?
3. Will only the `brightest minds’ be able to meaningfully contribute to research mathematics?
4. Will mathematicians be employable? Will mathematicians be needed?
5. Should I pursue a PhD in math at this time?

In this essay I will try to address these questions to the best of my ability, but will start with two disclaimers, followed by a brief summary of my own outlook.

Disclaimer 1. My answers may “age like milk,” as YouTube commenters love to quip on older videos. I can live with that, because this post expresses how I and many of us in the community around me feel today. Things can change quickly, though (see Disclaimer 2). I also want to acknowledge my privileged point of view as a tenured professor in mathematics — the situation can look much more troubling from the point of view of the job insecurity of a very early-career mathematician.

Disclaimer 2. No one has the answers at this time. I want to make clear from the start that no one can know with certainty the answers to any of the questions posed above: not any particular Fields medalist, not any given mathematician, not any particularly vociferous AI expert, and not the frontier model companies. And if someone is telling you with extraordinary confidence what the future holds, then I would immediately distrust the motives of their conviction (anecdotically, almost anyone on X.com that predicts the triumph of AI and the demise of the mathematics profession, is either a self-proclaimed “AI expert” or works for an AI startup). No one has a clear picture because development of LLMs has been so fast (and opaque) that it is almost impossible to predict what is to come. A good piece of advice is to ask the same questions to many people, to hear a (hopefully balanced) range of opinions. To that end, I am collecting interviews with mathematicians in what I call the “Human Mathematicians in the Age of AI” video project. I encourage you to listen to the interviews for some fantastic points.

For the record: I do not have the answers either, but I am hopeful and excited for the future. I will explain why below.

Who is controlling the narrative about LLMs in math? Overall, the mathematical community’s reactions to the advances in AI have ranged from confusion to anger — but, mostly, confusion about how to proceed. The most dystopian predictions seem to be driven by the fact that the so-called frontier model companies (and other LLM-powered companies) are controlling the narrative in the best of their interests. Unfortunately, the best corporate outcomes for an LLM company could have potential catastrophic outcomes for the math (and scientific) community.

It is certain that AI companies want us to believe that their products will imminently achieve “super-human intelligence” and that, in particular, they will be able to autonomously solve any mathematical problem a human could solve with or without the aid of an LLM. It is in their best corporate interest that the public is convinced of the (allegedly) “unlimited potential” of their technology, particularly before their companies’ stocks go public (i.e., their upcoming IPOs: Anthropic in November 2026, OpenAI in early 2027, etc). Thus, they have tried to control the narrative by spending a huge amount of (human and computational) resources in order to find solutions to certain well-known mathematical problems. The proofs are then released in announcements that lead the public to believe that their models can already autonomously solve any problem at all, and swiftly at that. However, this is (currently) far from their true capabilities. For instance, they never discuss how many tokens have gone to the trash bin with no payoff in trying (and failing) to solve famous problems. We do know, for example, that OpenAI invested the equivalent of some $15M to solve (err, scoop) the Navier-Stokes problem, but we are unaware of the surely colossal running cost of the failures to resolve other Millennium Prize problems.

My own outlook. Even though I am concerned about the incursions of LLMs into academic mathematics, I am quite hopeful. In fact, I consider this to be the most exciting time in my mathematical career (since the year 2000 say). Truly, this may be the most thrilling moment in mathematics in the modern history of our discipline, and I would be terribly sad to see young people leave academia and miss out on the stunning opportunity to be at the frontlines of the current scientific revolution. And not just sad: I think their absence would have disastrous effects for the field.

Undoubtedly, LLMs are already an incredibly powerful tool. If used correctly, and if we set up sensible academic conduct expectations around the use of LLMs, these tools can accelerate progress in our discipline unlike in any previous era. I fully expect that we, the community, will adapt and adjust to this new period, and we will harness these tools to achieve truly great things that just a few months ago seemed far out of reach. And I fully expect that human mathematicians will be front and center in these wonderful achievements to come. I will add reasons that support my optimism below.

I also want to add at this point that the day-to-day of a mathematician has not changed much so far! My days are still filled with teaching and joyful conversations about math with colleagues and students, doing research on a number of exciting (old and new) projects, and going to stimulating conferences to learn and disseminate our most recent methods and findings, while spending time with colleagues that make the mathematical community so wonderful and vibrant. Daniel Litt mentioned the same sentiment in a recent tweet.

One thing has changed though, I am busier than ever before, because the number of research projects I am involved in has tripled in just a few months. My research horizon has expanded significantly, and I have many more projects available for students to help me with.

Now, to the pressing questions:

“Will AI surpass the mathematical research ability of any human?” This is completely unclear. On one hand, the current trajectory in capabilities is surely significant, and we have already seen many impressive results that have been either proved by LLMs, or their proofs have been made possible thanks to substantial LLM contributions. On the other hand, none of the proofs so far seem to contain “alien ideas,” a move-37, or completely novel arguments or new concepts that were not present in the literature in some form or another. This should not be shocking because the LLMs are built and trained on the entirety of all human contributions to date, so it stands to reason that they would `think’ within the boundaries of our current knowledge and make connections (sometimes surprising and ingenious!) among ideas that are already present in the literature. I am particularly fond of the hypothesis (or toy model, as he called it) put forward by Nestor Guillen in a recent blog post, where he argues that LLMs may work within the confines of the convex hull of ideas that are currently available in the literature.

Take, for example, the disproof of Erdos’ unit-distance conjecture. We can imagine the current set of mathematical ideas as a stellated high-dimensional polytope, and we can place the state-of-the-art ideas on discrete geometry at an outer vertex and our knowledge on algebraic number theory at a different outer vertex. The idea for the proof seems ingenious at first sight because it cleverly mixes strategies from two fields of math at the vertices of the polytope of ideas, but after closer inspection, it’s a proof that was within reach of humans as it just sits within the convex hull of the polytope.

The polytope of ideas

This agrees with what Melanie Matchett-Wood said about the proof of the unit-distance when it was released: “I believe if the level and type of human expertise that is represented on this note had been assembled to find a counterexample to this conjecture a month ago, and those people put in similar amounts of time working on it than they did to reading and thinking about Chat GPT’s solution, the mathematicians would have found a counterexample.”

However, a proof of the Riemann hypothesis, say, may need new ideas that are strictly outside of the convex hull of current mathematical ideas, and it is therefore out of reach for an LLM. Only after a new idea is introduced in a new paper, the polytope of ideas may acquire a new outer vertex. And only then the LLMs, after being retrained to include those ideas, may fill out the set of results up to the new convex hull, which may or may not include yet a full proof of Riemann.

The convex hull of ideas

If this toy model holds up, then we would indeed expect the very fast advances in mathematics that we are currently seeing. As the LLMs take advantage of the stellated nature of the polytope of ideas, they will continue to fill in gaps between outer spikes. But as the LLMs fill in the convex hull with new results, we will see a deceleration in the number of results being shown solely by artificial intelligence. We will need human advances and intuition to generate new ideas that expand our knowledge polytope.

Even if the mathematical capacity of the LLMs (or future AI models) can at some point reach beyond the convex hull of the current set of human ideas, there is a different way that we may reach a limit to the LLM capacity: feasibility and ethical use of resources (this is similar what fellow optimist Kevin Buzzard called the “natural boundary” in a recent blog post). Is any cost (a dollar amount, human cost, ethical cost) acceptable in the pursuit of solving a given problem? Should we spend millions of dollars and an undisclosed amount of natural resources in order to find a solution for Navier-Stokes? As an analogy: we would like to know if there is life on Mars, but in order to do so as soon as possible, we would need an absurd amount of funding and risk the lives of a human crew in the process. Is it worth it? Similarly, we may reach a point where an LLM could solve an important problem for an exorbitant cost (in terms of funding and resources) but it may just not be an acceptable cost for the taxpayer or society to bear. Instead, we will need humans to devise an alternative route (the equivalent of a gravity-assisted robotic mission to Mars) to solve the problem at an acceptable cost, that produces a similar result in terms of mathematical advances and, more importantly, human understanding.

“Will research mathematicians become `professional prompters’ and interpreters of LLM output?” There is no indication that this will be the case. Yes, LLMs have produced proofs of important results somewhat autonomously (according to the frontier model companies — see Disclaimer 2) that some mathematicians have been tasked with interpreting and digesting. But in my own experience, and other research mathematicians who are using LLMs in their research seem to agree, working with an LLM is akin to discussing a problem with a collaborator, and the results heavily depend on how much guidance and intuition the mathematician inputs into the conversation. In other words, the LLMs are more than tools: they can be research collaborators but, as in any collaboration, the experience and the results are greatly improved when all parties contribute to the discussion. Further, mathematicians have no desire to prompt “solve the Riemann hypothesis, make no mistakes” and then interpret the proof. We prefer to be active participants during all the steps in the process of the discovery of a proof, because we are motivated by the `why the result is true,’ more than by the final answer that `the statement is true.’

Also, if we buy into the previous concept of the convex hull of ideas, then at some point in the near future it will be impossible to make progress in mathematics without a human adding a new idea, a new definition, a new concept that creates a new spike in the polytope, and then progress can occur.

“Will only the `brightest minds’ be able to meaningfully contribute to research mathematics?” At any given time in the history of mathematics, there have been mathematicians who are research active, and whose mental capacity for mathematics seems completely super human (e.g., the owner of this blog, among many others). It is natural to surmise that they could solve any problem we could solve, in a fraction of the time it would take us to complete a proof and write it up. However, this has never stopped those of us with a more modest capacity for mathematics from enormously enjoying doing research, and producing results that are far from insignificant. In fact, mathematics has always benefitted from the range of ideas and points of view, from the very concrete to the big bird’s eyeview, from the smaller contributions to the building of entire new theories.

Similarly, I am not threatened by the mathematical capacity of LLMs. For one thing their capacity is currently limited, as pointed above. And for another, even if their capacity becomes far superior, there will always be a need for mathematicians at all levels to guide research in paths that make sense for humans to walk (not run).

The mathematical universe is enormous (as Emily Riehl said), and computing time is finite. There will always be areas of mathematics that are under-explored and where even beginners can break new ground. The LLMs can help in the process, by quickly exploring avenues that may be dead ends, pointing out paths that have already been explored, and shining a light on paths that are likely to be fruitful.

As I mentioned above, I have never been this busy, because the access to LLMs has multiplied the number of areas that I have access to, and my curiosity has expanded well beyond my research area. I now have many more ideas that I can possibly explore on my own, so I am recruiting more student collaborators than ever before, to help me test whether these problems can lead to interesting results. Students can be involved in research earlier than ever before too because the LLMs can help them learn material faster (and deeper!), by virtue of being available 24/7 to answer their questions, instead of my meager one or two available hours per week to meet with them.

“Will mathematicians be needed? Will they be employable?” I find these questions natural but also perplexing. Even in the most dystopian of scenarios where AI becomes super human in all research tasks, what good would a proof (of a theorem in pure mathematics) be if there are no human mathematicians to digest it and understand it? Regardless of the advances in LLMs and AI, there will be mountains of research to be understood by humans, with or without the help of a computer.

In addition, we seem to forget that mathematics departments exist in universities to serve two primary goals: discovery and communication of mathematical knowledge. Virtually every mathematics department emphasizes, in equal parts, our research and educational missions (and many institutions place the educational mission of mathematics at a much higher level than their research mission). Mathematics courses are an integral part of a liberal arts curriculum because learning to think as a mathematician is a highly useful and applicable skill. The fact that we are researchers adds immense value to our educational goals, because students are best served learning from those scientists who are in the frontlines of research. The research opportunities that we provide for undergrads are a very valuable add-on to their curriculum, as it is a different type of training that helps them be employable in the future. And as long as the mathematical way of thinking continues to be a highly valuable skill to be learned by the undergraduate population, there will be a great need for mathematicians to be hired by universities.

The LLMs are making math research more accessible than ever to those who are not even in academia or even mathematicians. This means that undergrads will be able to join actual mathematician-led research projects much more easily, and it may be a new fertile ground for exploration. Not mindless exploration, though, but mathematical exploration where the goal is understanding and for the students to be initiated and trained into a highly technical field (in an ethical way). And, of course, we should prioritize training students in how to communicate the mathematics they learn, as that has always been (and probably will become even more of) a crucial skill.

All of this to say that I cannot conceive that the LLMs will displace mathematicians from their jobs. On the contrary, they might produce jobs since our research productivity may sky rocket. On the other hand, I am more worried about policies and funding issues that are political in nature and have nothing to do with the AI and LLM conversation.

Finally, the most important question of all, that I wanted to address here:

“Should I pursue a PhD in math at this time?” The answer to this question should be personal to each and every student. But, in my opinion, the answer should not have changed from a year ago to today. The most important reason (and perhaps the only reason) to do a PhD in math should be that the candidate is passionate about mathematics and wants to become an expert in a particular topic within our field. If that is the goal, then the presence of LLMs in mathematics is irrelevant, because the goal is achieved when the candidate has gained sufficient knowledge to be an expert on a particular problem. If anything, LLMs may be used as a tool to achieve that goal more efficiently. For one, I am using them every day to finally understand concepts and techniques that I always had questions about, and now I can query an LLM until I am fully satisfied. I am able to search for the explanations and examples that click with me, that click with my own particular way of thinking about mathematics.

To what degree a student wants to use LLMs in a math PhD should be a personal choice but I will say that, as my colleague Jeremy Teitelbaum put it in a recent interview (here is the bit I am referring to, and here is the full interview), students cannot afford not to learn about the current capabilities of LLMs, or any other technology for that matter. If your goal is to become an expert, then you have to be amenable to learning from all experts in the field, and from all sources that may allow you to go deeper into a subject than anyone else before you — and LLMs can be extremely efficient tools to explore literature, for instance.

But once again, the decision to do a PhD should not be based on the current state of the art of technology.

I wanted to do a PhD in mathematics because it seemed like a magnificent challenge. I wanted to do a PhD because I wanted to learn how Andrew Wiles proved Fermat’s Last Theorem. I wanted to continue studying mathematics because I simply did not want “a real job,” and the opportunity of contemplating advanced math on my own for a few years seemed like a dream to me, just too good not to give it my best shot. I know I would have deeply regretted it if I had not tried to complete a PhD when I had a chance (the best time to do it is when your undergrad knowledge is fresh!). I wanted to hear mathematicians talk about math, and rejoice in the small little details and miracles that make proofs work. I wanted to meet and hang out with other people who also thought number theory was the coolest thing on Earth. I wanted to publish a paper in a research journal, with my name on it, because I discovered a new theorem that no one had thought of before. I wanted to explain and share my passion for mathematics with others in a classroom and outside of the classroom.

Simply put, I just wanted to do math, and I would have been devastated if some undefined threat to the field of mathematics scared me away from the opportunity to pursue a PhD.

And if you are a student that is passionate about mathematics, and someone who wants all of that too, then a PhD is the right path for you, regardless of the technology available during your degree. You will learn to use the technology to a degree that you are comfortable with, and that fulfills your own dreams and expectations of what a PhD in Mathematics means to you.

Afterword: the BIG OpenAI release. After I finished writing this blog post, and had already sent it to Terry, OpenAI released a huge treasure trove of results in mathematics. This is, undoubtedly, a historic time in mathematics. The theorems in their papers prove some huge open problems in mathematics: the resolution of the so-called quasi Riemann Hypothesis, Goldfeld’s conjecture, the Hodge Conjecture in the case of CM abelian varieties, Hilbert’s 10th over Q, the Rigidity Conjecture… and the list goes on and on.

But such a tremendous release does not force me to change any of the points I made above. On the contrary, we already knew their models can do amazing things (e.g., Navier-Stokes). We already knew the frontier models can connect dots in the existing literature in ingenious ways (e.g., unit-distance conjecture). We already knew that OpenAI can spend a mind-boggling amount of resources to attack problems.

Also, we suspected that their models have limits and the new release shows evidence of that too. In their report, they mention that they attacked 4000 open problems, and their model was able to make progress on about 700 related problems. Yes, some of the ones they were able to solve are huge. But it also shows that their models are limited, quite possibly due to the arguments we explained above.

Are any of the solutions using new ideas that are outside of the convex hull of the current ideas in the literature? We will need mathematicians and time to digest these new proofs and understand what connections are being made, and whether brand new ideas were actually discovered in the process.

The main point of my post remains the same, though. There is a lot of mathematical research that remains to be done with and without the aid of LLMs. There are new mountains of mathematics to explain and communicate to others. And if you are a student who is passionate to learn what is new and what is left to do, then a PhD is definitely the right path for you.

[This is a guest post by the Association for Human Mathematics, reposted from their statements page. This blog post was initially written in a different file format and converted using AI. — T.]

Yesterday, on October 6th, 2026, OpenAI — which is currently defending lawsuits against accusations of illegal plagiarism, copyright infringement, and trademark dilution — released a repository of manuscripts purporting to contain solutions to a number of high-profile problems in mathematics.

Mathematicians did not ask for this work to be done. The Advisory Group on Mathematics and Artificial Intelligence, from whom OpenAI has claimed to derive its legitimacy, opened their initial advisory statement by saying that frontier AI corporations should not test advanced mathematical problems on internal models. In ignoring the central premise of the Advisory Group’s position, OpenAI has indicated total disregard for the norms of scientific research — norms that guarantee that mathematics remains trustworthy, ethically researched, and in the public interest.

Mathematicians have a particular vision of progress that is informed by history and field-specific considerations. We reject OpenAI’s assertion that this release advances our subject, and we urge mathematicians and the public to view the value of this publication model with due skepticism.

Releasing over 700 files at once is not a demonstration of scholarship, but a demonstration of power. We urge mathematicians to discontinue their work with OpenAI and to return to a vision of science that centers human understanding.

Association for Human Mathematics Communications Working Group

[This is a guest post by Raghu Meka. This blog post was initially written in a different file format and converted using AI. — T.]

“This problem has been tried by several famous mathematicians.” “There is a heuristic argument for why these methods cannot work.” “Getting this algorithm would give new circuit lower bounds.” Observations like these can take on a life of their own, almost like a game of telephone. A limitation of a particular approach, or an implication whose difficulty we do not fully understand, becomes a reason to believe that a problem is beyond reach, and eventually a reason not to think about it at all.

Over the past few weeks, I have been thinking about the role such perceived barriers have played in theory as I know it, and perhaps more broadly in mathematics. The recent articles on this blog about what it means to do mathematics in the age of AI have been very helpful in understanding and gathering my own thoughts. Looking back at several great results from the past year or so, a few of them (small fraction, admittedly) make me think that perhaps we lost some edge by imagining barriers–“social” hardness or limitations of approaches passed down as folklore–where none existed.

At least some of the solutions coming out of AI models, while brilliant, are also not completely alien. Yet these were problems we had almost stopped trying to solve, apart from small pockets of researchers. Of course, it is easy to say this post hoc. But in some sense, we have seen more `similarly brilliant’ solutions to newer problems than to these older ones. This makes me wonder how much our inherited perceptions have shaped where we were willing to look.

This has also made me think about some things from my early research days as a graduate student.

When I was a graduate student, I gave a talk on a small result. A very perceptive member of the audience (Adam Klivans, if you are reading this!) asked a question that I thought was a great one. But I also thought there were barriers around it, and it did not seem doable. Later, an answer to that question turned out to be an important piece in others’ resolution of a central question. The point of the story is not whether I would have solved the problem; probably not. The point is that the perceived barrier kept me from making even a half-decent attempt at it.

On a personal level, my progress in research was slow. If you are in mathematics, this might not seem that odd, but in theoretical computer science, having only one paper after five years, and that too not in one of the flagship conferences, could generally be taken to mean you had fallen well behind the curve. I nearly left theory. It was my mentors who pointed out that even if the results were not there, the failed attempts showed intent and progress, and that the absence of results was not evidence of a limitation I had begun to imagine. That support got me through then. They taught me not only how to do research, but how to love it.

Several times, I have had an initial impression that there were well-known methodological barriers, or a certain “social hardness” attached to the names of people who had attempted specific problems and directions. The research wisdom of some colleagues, and curiosity itself, helped me get past these impressions and engage with the questions. Pure curiosity is one force that can mitigate these perceived barriers; having people who are very optimistic (research-wise) or encourage that curiosity is another. Perhaps we need to cultivate this more.

Coming back to the present, I think this moment calls for extra care in resisting the trap of perceived barriers, and for revisiting several such accepted hurdles with less deference. We seem to have a mighty tool that can break through some of them. There are many problems whose solutions I thought I would never see, but now, by the universe’s grace, I will likely have the fortune to see them (perhaps some are already gathering dust on servers).

Relatedly, I also see a temptation to put implicit barriers on what “human mathematicians” can contribute. I wonder whether this might become the latest received wisdom that we accept too quickly. My predictive powers are quite limited. But even so, perhaps the epiphany I am having now is that the downside of not believing there is a barrier is far less than that of believing there is one. The cost of disbelieving has, after all, also come down because of the additional firepower we can now call upon. I would like to give curiosity a little more room before deciding what we can contribute, or what we cannot do.

To take poetic liberty, and borrow the words of Blake that gave Huxley his title: “If the doors of perception were cleansed every thing would appear to man as it is, infinite.”

Acknowledgements: I thank several friends who gave useful feedback on the first draft. AI was used to correct grammatical errors and polish sentences.

[This is a guest post by Ben Antieau, cross-posted from his blog. — T.]

There was no personal problem, no world problem, whose eloquent solution did not exist— somewhere in some hexagon.

—Jorge Luis Borges, “The Library of Babel” [1]

New repository

I am writing to announce Hexagon, a new repository for research works in the mathematical sciences and theoretical computer science. This has been a joint effort of many people over the last couple of months, starting in early August 2026. We felt that the proliferation of results proved with LLM assistance required a new model for collecting the associated papers. Besides wanting these works to be citable and reliably stored for long periods of time, we wanted to allow lower barriers for authorship and for community interest than the arXiv. We also wanted for these works to have a home besides random GitHub repositories or X/Bluesky/Mathstodon/LinkedIn posts.

In order to support the development of this project, we founded the Hexagon Mathematics Foundation in the state of Delaware and we intend to apply for recognition of tax-exempt status under section 501(c)(3). The Board of Directors consists of Mohammed Abouzaid, François Charles, Bryna Kra, David Savitt, and Lauren Williams. I serve as the first Executive Director. And, we have a wonderful Advisory Board, where Kevin Buzzard, Akhil Mathew, Johannes Schmitt, Steinn Sigurðsson, Nikhil Srivastava, Ravi Vakil, and Rachel Ward serve. For more details, see our who we are page.

My personal interest

When working with a group of people brought together by an FRG grant, we clicked a button and discovered a new result, namely derived invariance of Hodge numbers of fourfolds in characteristic zero. In the past, this would be a result I would have submitted to an excellent, but not top, journal. In this case, there is no way I would put my name to the result. Instead, I blogged about it here. This is a brittle way to aggregate mathematics. Now, it is on Hexagon as hexagon:2609.00104.

The creation of new results happens naturally in working with LLMs. They bubble up, even as side results. My personal hope is that it becomes the community standard to identify these and submit them to Hexagon.

The Lifecycle of Hexagon Objects

(The title alludes to Ted Chiang’s “The Lifecycle of Software Objects” [2].)

My ambition is that Hexagon is where mathematical ideas emerge from the water for the first time as they evolve toward community acceptance and understanding. Later, they should be written up in forms suitable for arXiv submission, publication, and canonicalization (Tao [3]).

Hexagon specifically allows submissions entirely generated by LLMs and even where the submitters claim no human understanding. These results should be available to the general community.

Submissions by the big labs

Hexagon welcomes submissions by large labs working on language models. These results should be available to the mathematics and TCS communities by default on a platform that the community maintains. We also welcome submissions by large collaborations or other organizations.

FAQ

How was Hexagon created? At some point, a group of people convened in early August, brought together by our social networks with the common theme of interest around creating a home for mathematical results which were rapidly being produced with the assistance of LLM tools. This group included most of the current members of the Board and Advisory Board of the Hexagon Mathematics Foundation, as well as several other academic mathematicians who did significant work but preferred not to be named. In August we discussed ideas on a private Zulip channel (thanks ICARM!) as we started building the site itself.

We talked to a lot of people at that time, including arXiv leadership, and we also examined closely-related AI-era repositories. From the arXiv we learned that they were not going to provide the home for these results we were looking for; instead they are focused on maintaining their project as it is today, and I am happy for that. None of the other repositories had gained sufficient traction or had all of the policies we were hoping for.

The foundation was incorporated as a nonprofit in Delaware and we intend to apply for recognition of tax-exempt status under section 501(c)(3).

The entire system was created with the help of OpenAI’s Codex and is hosted on widely available commercial cloud servers. This is rather easy nowadays. What takes time is deciding exactly what features you want and carefully writing the text on the website.

How is Hexagon funded? So far, it is entirely funded by the people involved, although we are exploring other funding routes and paths to sustainability. Today, except as customers of cloud infrastructure companies, we have no relationship with any for-profit company or other organization.

Why Hexagon? At some point, the group started talking about names involving Babel, which refers to Borges’s story The Library of Babel [1]. But, because it has other connotations as well, we did not go that route. Instead, someone suggested Hexagon in reference to the shape of the halls in Borges’s library.

Does Hexagon accept micro-results? Hexagon welcomes small, incremental improvements as long as they are of interest to the mathematics and TCS communities.

Is formalization required for a Hexagon submission? No, Hexagon is not primarily a formalization project, but it links to formalization projects, like mathlib, Palomar, prove2.me, and TauCeti.

What is the difference between a contributor and a submitter? On Hexagon, Contributors are humans or organizations responsible for the creation of submissions. Submitters are humans with ORCID-validated accounts on Hexagon. In some instances, Hexagon will provide individual account holders the capability to submit on behalf of other humans or organizations.

Are there rate limits? Yes, Hexagon limits the rate at which one can submit. It starts at 1/day, and grows at Hexagon’s discretion. This growth is based on previous submissions passing through moderation. (The arXiv recently announced its own repository-wide submission limits [4].)

Is there API access? Yes, Hexagon provides both read-access via API (in the style of the arXiv) and submit-access via API tokens available from users’ account pages.

Why is Hexagon marked as being in beta? We are still adding features and testing scalability. We welcome any recommendations for how the site can be made more usable.

References

[1] Jorge Luis Borges, “The Library of Babel,” translated by Andrew Hurley, in Collected Fictions, Penguin Books, 1999, publisher page.

[2] Ted Chiang, “The Lifecycle of Software Objects,” in Exhalation, Vintage, 2019, publisher page.

[3] Terence Tao, Mathematics in the age of AI, 2026, arXiv:2608.16753.

[4] Kat Boboris, Fair Moderation, Equitable Access, and AI: arXiv’s Updated Rate Limit Policy, arXiv Blog, 1 October 2026, article.

[This is a guest post by Thomas Bloom, crossposted from the Erdős problems forum. This blog post was initially written in a different file format and converted using AI. — T.]

AI is changing everything, for better and/or worse, and the rate of change is dizzying; in recent months this has been particularly evident in mathematics, where AI has gone from being essentially useless to helping solve some of the hardest problems in mathematics in less than a year.

The website http://www.erdosproblems.com has often been on the front line of these changes, and a barometer by which one could measure AI capabilities. This was not at all my intention when I created the site — I wanted to promote these problems to a human audience, and make a useful reference on what work has been done. But the easy availability of a large pool of questions that are simple to state, ranging from easy and obscure to deep and impenetrable, provided the ideal showcase for AI.

In some ways this has led to a huge amount of progress — we now know the answer to many questions we did not before. (Although a lot of this recent progress has come from increased human efforts and renewed interest in some problems, rather than just AI solutions.) There have also been negative effects, however: some mathematicians have dismissed Erdős-style mathematics as ‘easy/recreational’; many have stopped thinking about Erdős problems believing that they cannot compete with AI; and, most significantly, there has been a wave of AI-produced solutions provided with no explanation. While of course these are useful and tell us new things, they are also displacing and discouraging those who are actually interested in the mathematics.

(These issues have stopped being Erdős-specific as AI continues to make breakthroughs in an ever wider range of fields.)

A couple of weeks ago I asked for feedback on how people used the site, and what they thought should be changed. I received, both publicly and privately, a wide variety of opinions, and I’m grateful to everyone for their feedback.

What was particularly striking was the number of people I heard from who have benefited a lot from the site, learning new mathematics and finding new problems to think about, but have never commented on the site. I have been particularly conscious of this large silent, audience, and have tried to make sure their experiences were not drowned out by the more vocal minority.

In this post I will describe the changes I am making, based on the feedback I received and my own reflections on what the site is and could be.

In the essay ‘Why Do We Need Human Mathematicians Anymore?’ Po-Shen Loh suggests the following as an axiom to use when deciding how things should develop: We (humans) should help humanity flourish.

When thinking about what I should do about the site, I use the following variant:

http://www.erdosproblems.com should help the Erdős-community of humans (defined as those who are interested in Erdős-style mathematics, and want to think about and understand it) flourish.

Why change?

I launched http://www.erdosproblems.com on 28th May 2023, with just over 200 problems; it has grown steadily since then. The biggest change came in August 2025 when I added a comment feature. The site now hosts 1221 problems, over 9000 comments, and almost 2000 registered users. The site typically receives between 10,000 and 25,000 unique visitors each day.

The first few months after introducing the comment feature saw a huge increase in activity, just as I had hoped. A vibrant community arose; people shared ideas on how to solve problems, made observations, gave corrections, and suggested missing references and solutions. Many papers were written and new collaborations formed.

Unfortunately, this level of activity has not been sustained. Some decline was inevitable: over time, many of the natural observations will have been made, mistakes corrected, and discussions between collaborators would move offline. This natural evolution has been dramatically sped up by the coincidental rise of AI and its ability to solve some problems with minimal human intervention.

The main way that people publicly interact with the site now is to advertise their AI-generated proofs, often without any attempt to explain them, but as a way to record a (increasingly meaningless) priority claim.

This is very different to what I imagined, and I don’t want to manage a website which does this.

I believe that websites with this function should exist — places where people can record AI-generated proofs, even if purely formal with no human understanding, to save others wasting their tokens generating the same proof, and so that other people can access and use them if they desire. There are now several candidates for such repositories, and if managed responsibly, they can serve a useful role in the mathematical ecosystem. I personally don’t want to manage one.

Just as one does not open a restaurant in an abattoir, it is important that there be a separation between such repositories and a site which aims to promote the actual questions, place them in an appropriate context, and give a useful overview of the current state of human understanding.

The situation as it stands muddies the waters, promotes a gamified glory-seeking attitude, and gives the wrong impression that the value of these questions ends as soon as someone posts a formal proof of their truth value. This is not true (regardless of whether this proof was human or AI generated).

I believe Erdős intended these questions to serve as enduring beacons for human curiosity and wonder. They are landmarks by which we measure how far we’ve come, and how much there is still to understand.

I am very proud to have helped foster an open online community to discuss Erdős problems, and the kinds of discussions that used to happen are very valuable. But these discussions have become much less frequent. If and when I can find a way to encourage such discussions again, without the site becoming an AI repository of the kind mentioned above, I will happily do so.

What are the changes?

I will make the following changes. (As ever, these are somewhat experimental, and may themselves change and be clarified further in the next few weeks.)

1. A hiatus on problem comments and proof claims: I will freeze new problem comments and proof claims. General threads and blog posts will remain open to comments. Problem comments and proof claims may be reinstated in the future. Until then, suggestions for updates can be emailed to erdosproblemsonline@gmail.com, and I will update the site manually as I see appropriate.
2. No problem statuses: The site will not display the statuses of any problems (e.g. open, solved, etc.). All problems will be displayed in the same neutral colour. The count of currently solved problems and the solved percentage will no longer be shown.
3. No credit/ownership language to describe future solutions: The site will continue to record relevant results and theorems, but will no longer use credit-giving language for a result (human or AI).
4. An emphasis on high-quality expositions: I will focus more on the proof expositions feature. People are encouraged to write in with their own expositions of proofs (whether these proofs are old or new, human or AI), and I will post those I judge to be high-quality. I am exploring other ways to encourage human exposition (e.g. an online seminar). Please contact me if you have any ideas.

I’ve tried to anticipate some of the questions and critiques of these changes below. (I may update this with other questions and answers in future depending on feedback.)

What about those outside of traditional academia, who are using AI tools to make advances in mathematics, but can’t post to arXiv/lack the knowledge or context to write up proper papers about their findings?

I will post links to correct formalisations and high-quality writeups, whatever the source, whether from a traditional academic or not. Papers should acknowledge their sources and honestly disclose how AI was use; where there is evidence of plagiarism or misrepresentation about AI use, I may decline to feature the submission, even if the proof is correct.

This is removing one, unofficial, avenue of publication; there are, these days, many others (even if you are also unable to post to arXiv). AI-assisted search tools mean that people will find your work if they are interested in the area as long as you post it to one of these sites.

I encourage everyone interested in Erdős problems to think about them, and to work on them if interested. If you have a proof (AI-created or otherwise) then you should take time to carefully write up the proof yourself (rather than asking an AI to generate a PDF for you). If you are unable to understand the proof you could reach out to someone else to help write this up.

But emailing you my solution is slower, and it might be some time before you update the site.

This is true; but there is no great rush here. As much as I like these problems, and think it is important that there are some people who do think about the distribution of prime numbers and the structure of graphs, these are not problems for which a formal proof will have an immediate impact on general society.

I will try to link to correct Lean formalisations (if verified on Palomar) quickly; proofs which are poorly explained, and not accompanied by a formalisation, I am unlikely to update the site with. (See below for more details.)

What’s the point? There are loads of other places I can post my proof.

Indeed; this is partially why I feel comfortable halting such proof claims on the site, since modern search tools (including AI) make it easy to find proofs posted online about problems you are curious about, even if posted in obscure places.

I would like to use the small amount of influence I have to avoid promoting low quality proofs, and not to give an added veneer of legitimacy where it is not deserved.

I could just make my own site for people to share their proofs and discuss solving problems with AI. Heck, I can even use AI to scrape all the text off your site and make an exact clone with much more liberal policies.

Yes, you could. This a period of great experimentation in different formats and ways to encourage mathematics; if you think you have a good idea for a site or resource, you should make it. (Although it is often better to help out an existing effort where possible, since these resources are only useful if people use them, and it is better to concentrate on creating a few high-quality sites than hundreds of very similar clones.)

I think it is, however, rude to use without permission the text from my site, which is the result of a huge amount of work from me and many others who have contributed to the site.

How long will the hiatus last for?

I don’t know. I will monitor how things develop in the coming weeks and months, and will reintroduce comments and proof claims (perhaps in a different form) when I believe they will do more good than harm.

Why not just moderate the comments to only allow genuine discussion through?

This has been tried; in practice the vast majority of the comments the site receives now are people announcing AI-generated proofs. It is not sustainable to have a moderation policy which would reject almost all the comments that are submitted.

I am open to alternative suggestions about how to create a space for human discussion and collaboration, either on the site or elsewhere.

What about existing comments and proof claims?

They will remain as an archive of the site up to this point.

Will you update the remarks to reflect existing proof claims?

Yes, I will be working through the backlog of existing proof claims and updating the remarks, linking to formalisations and so on, as appropriate. You do not need to email me about a proof claim already on the site.

How will you decide when to update the remarks? What can I do with my proof to help?

I will update the remarks when I judge there is an interesting new result that people who are working on that problem should be aware of, that can be presented in a useful way. Some things to be aware of:

1. If you have a Lean formalisation register it on Palomar — this lets others see that the formalisation compiles correctly, and makes it easy to check the formal statement correctly matches the problem statement. I will then link to the Palomar registry.
2. A proof accompanied by a well-written exposition that demonstrates clear understanding and which makes it easy for others to understand the proof will be prioritised.
3. If I judge there to be some kind of academic fraud (e.g. using the ideas of others without attribution, or passing AI-generated work off as your own) then I will not post it. This may mean that there are correct proofs not acknowledged, but the alternative is to publicise and reward bad behaviour. (As mentioned above, these proofs will surely still be found by anyone who searches for them elsewhere, but at least I would not be implicitly endorsing them.)

What’s the point in removing the problem status? Isn’t it just cosmetic, and doesn’t it just make the site harder to navigate?

Yes, this does undeniably remove some information. I think, however, that what is lost is not significant for anyone seriously interested in that problem, who can see for themselves within seconds of reading what the current situation is.

It makes it harder to browse the site searching for an unsolved problem to work on; instead I recommend that people browse the site by topic, finding questions that interest them, and investigating those, whether the original question is open or solved, since there is always more to be done.

The main point is to disincentivise people who are simply glory-chasing and copying problems into their AI to get an OPEN->SOLVED dopamine hit. It also prevents people drawing wrong conclusions from the ‘rate of solved problems’.

Furthermore, there is a lot of subjectivity anyway in many problems as to what counts as solved. Many people only browse the open problems, and they’re missing out on a lot of great mathematics that way.

I think it is against the spirit of Erdős to regard any problem as ‘closed’ — whenever one form of a question is answered, many others are created, and all problems deserve continued attention.

Doesn’t the ‘no credit’ rule also devalue the work of humans?

Unfortunately, yes. I anticipate this will only be temporary, while the norms and customs of this new age of mathematics are decided. The commentary on the site is in no way ‘official’, and just represents my own summary of the situation, and collects links which may be useful to others exploring a problem.

Information about authorship will still be available in the sources the site links to. I trust that people will be sensible enough to judge for themselves who deserves the appropriate credit, and reward them appropriately.

I will also be freer in my language when it comes to well-written papers, whether they are the first place a proof appears or explain a proof that originated elsewhere; but I will no longer use language that suggests anyone ‘owns’ a particular result or proof. (For example, instead of saying ‘Bloom proved that ‘, I will write ‘It is known that — an explanation of the proof is provided by Bloom [link]’.)

Erdős and AI

I am often asked ‘what would Erdős have thought of AI?’ The short answer is ‘I don’t know’. I never met Erdős, and have no special insight into him; I know him only through biographies and his papers, and anecdotes and reminiscences from those who did know him.

I would like to honour his legacy, and create something that he would have liked. To that end, I want to stress one thing: Erdős was, as well as a mathematician, an incredibly social person. Many stories about Erdős emphasises his humour, his warmth, and his enthusiasm for talking to other people (mathematicians or not). He spent his life travelling from mathematician to mathematician, arriving on their doorstep and declaring ‘my brain is open’.

He was not the type to lock himself away for years working in isolation on a single problem. For Erdős, mathematics was a very human activity, best done out loud. Questions would arise, be solved or discarded and replaced by new questions. Some results obtained, new ideas found, and then onto the next problem.

Some view the future of mathematics as a dystopian arcade of button-pressing, staring at a screen waiting for AI to do the thinking for us, with the main human involvement limited to asking the initial question and offering sporadic words of encouragement. Each new proof is then thrown into a repository, to only ever be read by other AIs, and the human presses the next button.

I believe Erdős would have found this future grim indeed, and the antithesis of mathematics as he practised it. Use AI as you like — but do not abandon mathematics as a human activity.

Don’t solve a problem for the sake of it; life is too short to spend it doing things that don’t matter to you.

Find a question that is meaningful to you, find other humans who are interested in it, and talk about it. Be confused, be stuck, be inspired. Find a messy proof, then find a better one. Get tired, get hungry, get into a flow state. Argue, laugh, give up, drink some coffee, and attack it again.

Be human. Let your brain be open.

[This is a guest post by Annalisa Buffa. This blog post was initially written in a different file format and converted using AI. — T.]

About us and the position

The Chair of Numerical Modelling and Simulation at EPFL is dedicated to the design and analysis of numerical algorithms for partial differential equations. Our research is oriented towards the development of novel and innovative numerical techniques aiming at improving the integration between numerical simulations and geometric modelling and processing.

Proof assistants such as Lean, together with recent AI tools, are changing how mathematics is done. We are opening a postdoctoral position to explore what formal verification and algorithm discovery can bring to numerical analysis. There is no fixed project. The goal is to find out, through concrete experiments, where these approaches help in the design and analysis of numerical schemes for PDEs, and where they still fall short.

What you will do

As a postdoc in our group, you will set up and lead this new research line, choosing its directions together with us. Possible starting points are the formalization in Lean of stability and error estimates for finite element methods, or the AI-assisted discovery of new discretization paradigms for classes of PDEs where standard methods struggle, with their properties then verified formally. You will publish and present your work internationally.

You are the ideal candidate if

• You hold a PhD in mathematics, computer science or a related field
• You have a strong background in formal verification with Lean
• You have experience in AI-assisted theorem proving or algorithm discovery is an asset
• You have working knowledge of numerical analysis, ideally numerical methods for PDEs
• You are independent and comfortable with open-ended research questions
• You communicate well in English and enjoy working at the boundary between disciplines

We offer

• A stimulating international environment at one of Europe’s leading research institutions
• Competitive salary and excellent working conditions
• A 1-year contract, renewable
• Freedom to shape a new research direction from the start
• A friendly team with strong postdoctoral and PhD researcher community

If you are interested

Submit your application containing CV, motivation letter, and contact details for 2 referees through this link. In the motivation letter, briefly describe one question you would like to work on, linking numerical analysis with formal verification or algorithm discovery. Applications will be reviewed until the position is filled. Start date: as soon as possible (flexible).

[This is a guest post by Jeremy Avigad. This blog post was initially written in a different file format and converted using AI. — T.]

“Mathematics underwent, in the nineteenth century, a transformation so profound that it is not too much to call it a second birth of the subject—its first birth having occurred among the ancient Greeks…”

Howard Stein, in “Logos, Logic, and Logistiké: Some Philosophical Remarks on Nineteenth-Century Transformation of Mathematics”

“The report of my death was an exaggeration.”

Mark Twain

“May you live in interesting times.”

(traditional)

I recently attended a meeting of innovative science and technology startups supported by Convergent Research, the organization that oversees the Lean FRO, a nonprofit that develops the Lean theorem prover. The meeting was designed to stimulate discussion, and when I introduced myself as a mathematician, many participants were eager to talk about the impact of recent events in AI on mathematics and reactions in the mathematics community. They were surprised to hear that I find the tone of the community responses on blogs like this one and Proofs and Prompts generally positive and encouraging, even though we all recognize that fundamental aspects of our day-to-day professional lives are bound to change. These discussions have helped me shape some of the thoughts I would like to share here.

There is a narrow view of what mathematicians do, encapsulated in our daily workflows: we try to solve problems, and when the hard problems are too hard to solve, we make up easier approximations, solve them, and then vary the parameters. That practice has been disrupted by the events of the last few months, in the sense that the kinds of results that would have, a year ago, made for perfectly respectable publications can now easily be generated with the help of AI. This has left us worrying about what it will mean to do mathematics going forward, as well as how to train and support the next generation of mathematicians to do whatever that is.

The history of mathematics offers us a broader view. What has remained stable, despite centuries of changes, is that mathematics is a culture of rigorous reasoning and communication, providing us with language and abstractions that let us think and communicate more reliably and efficiently. Surely such reasoning is still important, even in the age of AI. The fact that many of us find mathematics aesthetically pleasing doesn’t diminish its practical utility, but rather is explained by it: I expect that the reason that doing mathematics feels so good is that it is the exercise of capacities that are so fundamental to our survival as a species that they are wired into our DNA. If that’s right, mathematical thought isn’t going away any time soon.

The challenge is that solving the kinds of problems we have been solving for decades becomes decoupled from the goal of enhancing our mathematical understanding when we let AI do the work. The question, therefore, isn’t whether we still need mathematics, but rather how to pursue mathematical understanding in the age of AI. I will provide three general answers.

Solve harder problems

There are two salient features of today’s foundation models: first, they have seen the entire mathematical literature, and second, they are tireless; a swarm of agents can make its way to a solution by trying countless variations. This explains why the AI-generated solutions to open problems we have seen all have a similar character: they are problems that AI could solve by cobbling together available techniques. (I am grateful to Matthew Ballard for this characterization, and the subsequent analysis.)

Can every interesting mathematical question be answered that way? Probably not, and even questions that can may have more interesting and satisfying solutions that invoke novel ideas and insights. Perhaps, in the near future, AI systems will be able to come up with such insights, but, at the very least, let’s recognize that we are not there yet. Reinforcement-learning training regimes have systems chain conventional moves and learn, from a history of failures and successes, which ones are most promising in a given state. The fact that the value of an action is graded solely in terms of the success of a final trajectory breeds superhuman cleverness but may miss creativity and higher-level strategizing. In any case, there are still hard questions to be solved and ambitious research programs to pursue, and the possibility of making progress on them with the help of AI is exciting.

Think bigger thoughts

Our present situation would be much more depressing if mathematics were a matter of ticking off problems imposed on us by aliens, an endless sequence of exercises and exams. The good news is that when we do mathematics, we get to choose the problems, grade the solutions, and favor the ones we like best. We decide what’s interesting to us, what questions to pursue, and why. Our destiny is in our hands.

The things we admire most in mathematics often seem to come out of nowhere. In 1853, the young Bernhard Riemann submitted three potential topics to his advisor, Carl Friedrich Gauss, to choose from for his Habilitationsvortrag, a lecture he was required to give to secure a teaching position at the University of Göttingen. Gauss reportedly chose the topic for which Riemann was least prepared, to see what he would make of it. The resulting lecture, “On the Hypotheses Which Lie at the Foundations of Geometry,” was published posthumously in 1868, and it revolutionized the field. The lecture distinguished a space’s metric properties from its topological properties and introduced the general notion of a manifold, though the latter did not receive a fully rigorous treatment until the twentieth century. The focus on intrinsic properties of a space—in Riemannian geometry, those determined by the metric and independent of embedding in a larger space—was key to Einstein’s theory of general relativity decades later. Riemannian geometry has had applications that Riemann himself could never have imagined, from robotics and medical imaging to statistical analysis.

William Ewald’s excellent sourcebook, From Kant to Hilbert, provides a lovely introduction to the paper and quotes Felix Klein’s description of the work:

“The publication of [Riemann’s lecture] occurred just at the time when I was beginning to occupy myself independently with mathematical problems. So I still have vivid memories of the extraordinary impact Riemann’s train of thought made on the young mathematicians of the day. Much seemed to us dark and difficult to understand, and yet of unfathomable depth, where the modern mathematician, who has already absorbed all these things into his mode of thought from the outset, only admires the clarity and fecundity of the exposition.”

What seemed dark and mysterious to the young Klein is now part of the canon, something that foundation models have absorbed and internalized through their training, just as young mathematicians do. I am grateful to Ballard once again for suggesting this example and pointing out that no reinforcement-learning setup could have evaluated Riemann’s decisions: the benefits are diffuse and hard to track, and the time horizon is much too long.

The same can be said for countless mathematical developments that have opened up new vistas, such as Galois’ focus on groups of permutations in the study of solvability of algebraic equations, Poincaré’s qualitative studies of dynamical systems, or Grothendieck’s far-reaching conceptual innovations. Will AI eventually be able to make advances like these? That’s not even the right question to ask. Telling us that some AI agent is spinning out theorems that are highly interesting to it and other AI agents does nothing for us. We should care about AI only insofar as the results are interesting and important to us, and, at the end of the day, it’s up to us to decide what that means. The values we assign to mathematical developments are embedded in our history and culture.

Imagine planning a trip to go backpacking in the Alaskan wilderness for exercise and recreation. You might be happy to let AI help book your flight, but not to let AI take the hike for you and send you pictures. In mathematics, what is at stake isn’t our recreation but agency over our reasoning and deliberation. Whether or not AI can think, it can’t think for us. We have our own lives to live; mathematics is our story to tell, and it’s up to us to decide how to tell it. With AI, there’s even more to explore, and no shortage of avenues for discovery.

Try new things

So far, I have focused on using AI to help us do the things we used to do, but let’s not forget that the technologies themselves raise new questions, and that we have a lot to learn about how to use them effectively. I have argued in another essay (now scheduled to appear in the Notices of the AMS) that mathematicians should be actively involved in understanding how the technologies work and in coming up with novel and creative ways to use them to do new mathematics.

AI changing what it means to do mathematics is not without precedent. The use of algebraic methods to solve geometric problems in the seventeenth century was a new technology, and not everyone liked it; yet we mastered the new techniques and learned how to use them to great effect. The same is true of infinitesimals later in that century, algebraic structures in the nineteenth century, set-theoretic abstraction and structural language in the early twentieth century, and numerical and symbolic computation more recently. These were all alien and disconcerting when they were new. We should view those who invest time and energy in getting proof assistants and neural networks to help us discover new mathematics as doing mathematics proper, rather than dismissing them as mere technicians. In the age of AI, developing symbolic automation or training a neural network can be no less a contribution to mathematics than manually chaining inferences to prove a theorem.

I have heard arguments that as the job market contracts, we should turn inward to preserve traditional mathematical skills. On the contrary, I believe that engaging with new technologies and learning how to use them to improve our ability to reason and discover new mathematics will keep the discipline strong. Expanding our view of mathematics is the best way to expand the profession and keep it relevant.

Our message to the next generation

My rosy outlook on the future and glib advice to solve harder problems, think bigger thoughts, and try new things will not provide much comfort to students and early-career researchers, who feel the ground shifting beneath their feet. My words are not meant to diminish the challenges ahead or suggest easy responses to the disruption. Mathematics departments, community leaders, educators, professional societies, and journal boards are holding emergency meetings all over, and are doing their best to make concrete recommendations and take appropriate action. We have our work cut out for us.

Despite the uncertainty, there are some clear messages we can send to the next generation of mathematicians. The first is that we stand with you. There is nothing more important to us than the health and strength of the discipline, and ensuring that you can thrive. We have the humility to recognize that our experience and expertise are limited, and that some of the things we thought we knew in the past are no longer valid. We are committed to working with you as best we can to preserve the profession and keep it strong.

Second, mathematics is as important today as it ever was, and we need you. AI must not replace our collective ability to reason and deliberate, and mathematics remains a core capacity for doing so. We cannot imagine a world in which mathematics does not play an important part in our lives.

Finally, the next few years will be extremely interesting. We are at a new frontier, where our communal norms, values, and expectations are beginning to break down, and it’s up to all of us to figure out what should replace them. I am confident that future historians will see this moment as the start of a new era of mathematics, and that they will weigh the consequences of our actions and decisions. Mathematics has never been for the faint of heart; this is our opportunity to rise to the occasion and face the challenges together.

[This is a guest post by Diego Córdoba and Luis Martínez-Zoroa. This blog post was initially written in a different file format and converted using AI. — T.]

Euler formulated the equations for an inviscid incompressible fluid more than 250 years ago. Published in his 1757 memoir, they belong to the earliest systems of partial differential equations in mathematical physics, following d’Alembert’s work on the wave equation. Understanding the evolution they describe has required the work of many generations of mathematicians. One of the central questions is whether an initially regular fluid flow can develop a singularity in finite time. The recent work on Euler and Navier–Stokes obtained with the aid of large language models has brought renewed attention to this question. These exciting developments build on decades of mathematical research, including works from recent years, when the field has continued to be specially active. In this post we describe some contributions to that body of knowledge, including our own. We will go over some of that recent mathematical literature, and discuss the ideas of constructing blow-ups through a cascade of vortex layers.

Partial differential equations provide a common language for problems ranging from wave propagation and fluid motion to geometry and general relativity. For an evolution equation, the Cauchy problem asks us to determine the future from prescribed initial data. A local existence theorem gives a solution for a short time; the next question is whether it continues for all time or develops a singularity at a finite time. This distinction between global existence and finite-time blow-up is already visible in the elementary Riccati equation

The solution starts from a finite value and remains smooth until , when it becomes unbounded. The quadratic nonlinearity in three-dimensional Euler suggests a similar possibility, but the fluid problem also involves transport, geometry and a pressure determined nonlocally by the entire flow. The challenge is to understand whether the full equation can sustain the amplification suggested by this simple ODE.

The central aim of our research has been to construct classical solutions of incompressible fluid equations that develop singularities in finite time, starting within a regime of local existence and uniqueness. We want the initial data to determine a unique regular evolution for a positive interval of time, followed by a singularity at a positive, finite time. In the smooth-data setting, this means a solution that is initially smooth and stays smooth until the singular time. More generally, the local theory also applies to classical solutions with finitely many derivatives. This programme includes the incompressible porous media (IPM) equation, the generalized surface quasi-geostrophic (gSQG) equations, the Boussinesq system and the two-dimensional non-homogeneous Euler equations, with particular emphasis on the three-dimensional incompressible Euler equations.

Our approach developed through increasingly demanding constructions. We first sought mechanisms for rapid growth of regularity norms, then used them to produce instantaneous loss of regularity in critical and supercritical spaces. We subsequently arranged for singularity formation after an interval during which the local theory guarantees regular evolution. The distinction between these phenomena is an important part of the story.

Classical solutions and local existence

The incompressible Euler equations are

where is velocity, is pressure, and is an external force, which may be zero. The condition expresses incompressibility. A classical solution has enough differentiability for the equation to hold pointwise. This does not require infinitely many derivatives, nor does local differentiability imply that every global regularity norm is finite.

For unforced Euler in dimension , the classical local theory gives existence, uniqueness and persistence of regularity for initial velocity in , with and , together with suitable control at infinity, such as finite energy. Here means that derivatives up to order are bounded and continuous, and the derivatives of order are Hölder continuous with exponent . In Sobolev spaces, which measure square-integrable derivatives, local well-posedness, including continuous dependence in the same norm, holds in

The properties relevant here are existence, uniqueness and persistence of regularity. With a time-dependent force, a sufficient assumption in the finite-energy Hölder setting is ; in the Sobolev setting it is . The notation in time means that the indicated spatial norm of the force is integrable on every finite time interval under consideration.

Higher regularity is propagated as long as the solution remains controlled in the continuation class and the force has the corresponding regularity. For unforced Euler in two dimensions, these regular solutions exist globally. In three dimensions, the possibility of finite-time breakdown is tied to vortex stretching.

Writing , the three-dimensional equation becomes

Vorticity measures local rotation. The velocity transports it and, through the stretching term , can also amplify it. This deformation is generated by the vorticity itself through the nonlocal Biot–Savart law. This is the feedback that makes the Riccati analogy suggestive. A singularity construction must organize it while retaining control of transport and of the interactions between different regions.

For unforced three-dimensional Euler, the Beale–Kato–Majda continuation criterion states that breakdown of a sufficiently regular solution at a finite time requires

The same criterion has a forced version, provided the force remains regular in the appropriate time-integrated sense. For a velocity in with , one convenient sufficient assumption is

The second condition controls low frequencies. After absorbing the gradient part of the force into the pressure, these assumptions control the effective force in , and the usual BKM estimates apply. Thus, the threshold is for the curl of the force, corresponding to one additional derivative on velocity. A similar criterion applies in the setting of Holder spaces. The point is to rule out a breakdown caused simply by an inadmissible force. Our goal is to realize the required vorticity growth dynamically from a local well-posedness regime.

Instantaneous loss of regularity

A first warning is that local regularity propagation can fail at the borderline of the classical theory. The assumptions above cannot simply be replaced by their endpoints. Bourgain and Li established strong ill-posedness at the critical Sobolev regularity : for velocity in two dimensions and in three. Their constructions exhibit instantaneous loss of the critical norm. They also proved instant loss of regularity in the integer spaces , . Elgindi and Masmoudi independently developed another approach to ill-posedness in these integer regularity classes.

These results show that the borderline spaces need not support the regularity propagation available immediately above them. Having one continuous derivative does not provide the same control as a first derivative that is Hölder continuous with a positive exponent. For higher integer , instantaneous loss of the norm can also coexist with classical differentiability at lower orders.

An especially striking phenomenon is an instantaneous gap loss of Sobolev regularity. In our work with Wojciech S. Ożański, we construct global classical solutions of the two-dimensional Euler equations with finite energy for which, given any ,

for every and every .

The number on the right is strictly smaller than . Thus, the solution does not merely leave its initial Sobolev space: it immediately loses an entire positive interval of regularity. In velocity variables, the initial regularity is , below the critical space . This is a result in the supercritical Sobolev regime.

There is no contradiction between this loss of a global norm and the persistence of local classical differentiability. Definition 3 in that paper makes the distinction precise. On each finite time interval, the vorticity belongs to for some and is in space and time on every compact cylinder. It satisfies

pointwise, with the prescribed initial data. The constructed solution is unique within this specified class. Its local differentiability persists even though its global Sobolev norms become infinite.

The proof first constructs smooth solutions with arbitrarily large Sobolev norm growth. A nearly radial background rotates an oscillatory perturbation at different rates at different radii, creating finer scales. Carefully rescaled copies of these building blocks are then placed increasingly far apart. A gluing argument controls their nonlocal interactions and produces one exact solution with instantaneous gap loss. Spatial separation permits local classical regularity to coexist with the failure of global Sobolev control.

We have also investigated instantaneous loss of regularity for SQG and its generalizations, establishing strong ill-posedness in integer and Sobolev spaces, Hölder spaces, and, jointly with José Antonio Lucas-Manchón, supercritical Sobolev spaces for gSQG. These investigations include the construction of global unique solutions exhibiting instantaneous loss of regularity in the presence of supercritical fractional diffusion, and, with Wojciech S. Ożański, classical SQG solutions whose Sobolev regularity decreases continuously from the initial time. For IPM, our joint work with Roberta Bianchini establishes strong ill-posedness in for arbitrarily small perturbations of a linearly stable stratification, showing how the nonlinear dynamics can overcome the stabilizing effect of the background profile.

These examples make clear that instantaneous loss of regularity concerns failure of propagation in a chosen function space and can coexist with classical differentiability. The next challenge is to construct a singularity after a positive lifespan during which the relevant regularity is guaranteed to persist.

Singularity formation after regular evolution

Elgindi’s construction was a breakthrough in precisely this direction. It produced finite-time singularities for three-dimensional Euler in , for sufficiently small positive , using axisymmetric flows without swirl. The original exact self-similar profiles had infinite energy. Elgindi, Ghoul and Masmoudi subsequently used stability and localization to construct finite-energy singular solutions without forcing.

The initial velocity in these constructions belongs to a class in which the local theory guarantees a unique regular evolution. It is but not smooth everywhere. Axisymmetry means invariance under rotations around an axis, and “without swirl” means that the velocity has no component in the angular direction. Smooth flows in this class admit a global regularity theory under the usual decay assumptions, so the distinction between finite Hölder regularity and full smoothness is essential.

Recent work has clarified how close one can come to the boundary of this global theory. For the homogeneous, unforced axisymmetric Euler equations without swirl, global regularity is known for initial velocity with , under the corresponding finite-energy and decay hypotheses. Three recent approaches construct singularities below this threshold, for . Shkoller’s preprint uses a Lagrangian clock-and-driver framework, coupling the collapse of a flow Jacobian to the compressive axial strain. Chen’s work constructs asymptotically self-similar blow-up from finite-energy initial velocity, using computer-assisted estimates for a one-dimensional profile and an analytical construction and stability argument for the three-dimensional flow. Shao, Wei, Zhang and Zhang construct exact self-similar profiles with infinite energy and prove stability after controlling finitely many unstable directions. Their current manuscript also uses this stability to localize the profiles and obtain finite-energy, asymptotically self-similar singularities. These different methods reveal a sharp regularity threshold within a class that still has classical local existence and uniqueness.

Elgindi and Pasqualotto constructed singularities for Boussinesq and axisymmetric Euler with swirl, exploiting instabilities related to Rayleigh–Bénard convection and Taylor–Couette flow. Their argument uses a self-similar framework and includes a computer-assisted step in the proof of invertibility of a linear operator.

There has also been major progress for smooth initial data in domains with a boundary. Following the numerical scenario of Luo and Hou, Chen and Hou combined analysis with rigorous numerics to establish nearly self-similar finite-time blow-up in that setting.

Our work with Fan Zheng introduced a different route to singularity formation in the whole space: non-self-similar blow-up for unforced Euler, with finite-energy velocity in for small positive , smooth away from the origin. The solution is assembled from interacting vorticity regions at successively smaller scales, organizing the singularity through a hierarchy of amplification events.

A cascade of vortex layers

The basic idea is to arrange vorticity on a sequence of widely separated spatial scales. An outer layer generates a deformation that amplifies a more concentrated inner layer. Once amplified, that inner layer provides a stronger deformation for the next one. The time required for each stage decreases, and the sum of these time intervals is finite. In this way, infinitely many amplification stages can accumulate at a single finite time, while the solution remains regular on every shorter time interval.

Scale separation makes this interaction tractable. Across the small support of an inner layer, the velocity generated by the outer layers can be approximated by a simpler field. In the Euler constructions, this field has a hyperbolic structure, stretching one direction and compressing another. Aligning the vorticity with the stretching direction produces amplification.

The hard part is to realize this process in the full equation. The inner layers also affect the outer ones; each layer interacts with itself; and transport changes the geometry and frequency of the oscillations. We choose the layers so that crucial self-interactions cancel at leading order, while scale separation and oscillatory cancellation control the remaining interactions.

In the unforced construction with Zheng, we analyze finite collections of vorticity regions and pass to a limit of exact Euler evolutions. The full infinite hierarchy is already present in the initial data; the cascade describes the successive amplification of its layers. The construction is compatible with regularity and finite energy, though not with smoothness at the point where the scales accumulate.

The forced version gives further flexibility. We construct an approximate evolution and define the external force through its residual. The main difficulty is to arrange that this force remains in the required regularity class up to the singular time, even as the solution itself loses regularity. This requires precise control of the cancellations and of the errors at every stage of the cascade.

In our forced Euler construction, the velocity lies in before blow-up, and the force remains uniformly controlled in . The flows are non-axisymmetric. Thus the method reaches considerably higher velocity regularity while retaining a force in a classical local well-posedness class.

This is a useful way to view the programme: construct an amplification mechanism, then improve the accuracy with which it can be implemented in the equation. The quality of the error estimates determines the regularity of the force.

Adding dissipation

A particularly important test of the method is whether it survives the addition of dissipation. With Fan Zheng, we addressed this for the fractional Navier–Stokes equations

where . Ordinary Navier–Stokes corresponds to ; the range is hypodissipative. Classical results of J.-L. Lions 1969 establish global regularity when , starting from smooth, divergence-free initial data with suitable decay. Tao subsequently extended this theory slightly into the supercritical regime, proving that global regularity persists when the critical dissipation is weakened by a suitable logarithmic factor.

Our theorem constructs finite-time singularities for

with force

for some . The velocity is smooth in space before the singular time, and both its speed and its energy remain bounded. Nevertheless, after normalizing the singular time to 1,

The force has the time integrability and spatial regularity required by the local theory, so the singularity is not caused by a loss of admissibility of the forcing.

Dissipation cannot simply be added to the old construction and ignored. For an oscillation at frequency , the fractional dissipation term has size comparable to times its amplitude, so its damping time scale is approximately . The strain generated by the preceding layer has to overcome this damping. Increasing the frequency helps some approximation estimates, but simultaneously strengthens dissipation. The parameters must satisfy both requirements.

Section 1.2 of the paper explains why the earlier Euler choice of frequency separation fails in the presence of any positive-order diffusion. We have to redesign the relation between amplitudes, frequencies, support sizes and activation times. We also need an accurate approximation of the fractional Laplacian that preserves the structure used to analyze each layer. Cancellations in the nonlinear self-interactions remain essential to keeping the force in the required class.

This theorem shows that the cascade can survive a mechanism that actively suppresses the growth it is designed to create. Our result concerns small fractional powers of the Laplacian, not ordinary Navier–Stokes. The gap between this range of and is substantial; the ordinary Laplacian cannot be reached by simply rescaling this construction.

Smooth forcing and recent developments

The same programme can be applied to other incompressible models. Our IPM construction starts from smooth, compactly supported initial density and produces finite-time blow-up with a source uniformly smooth in space. The solution remains smooth before the singular time, while its norm tends to infinity as that time is approached.

Keeping the source uniformly in space requires increasingly accurate approximations of the velocity. As we introduce layers with higher frequencies, we use approximations of progressively higher order, with the approximation order tending to infinity along the cascade. In this sense, we need an approximation “of infinite order” to control the errors absorbed by the source in every spatial norm. The assumption was chosen to simplify the construction. As noted in the paper, smoother time cutoffs and a more careful analysis of the errors give regularity with additional work; we also anticipated that full smoothness in both space and time should be attainable.

Further developments include our Boussinesq construction with Andrés Laín-Sanclemente, based on multi-layer degenerate pendula, and its extension to variable-density Euler with source terms. Our work with Óscar Domínguez and José Antonio Lucas-Manchón on forced generalized SQG establishes finite-time blow-up in a Sobolev local well-posedness regime, for the parameter range .

Recent work of Alpöge, Buckmaster and Coiculescu extends the IPM construction to a source smooth in both space and time on the torus. The Boussinesq and Euler manuscripts of Alpöge and Buckmaster likewise state blow-up from smooth initial data with smooth forcing. These works explicitly build on amplification through successive layers. Their additional regularity requirement is to control every mixed space-time derivative of the forcing uniformly through the singular time.

OpenAI’s September 8, 2026 announcement concerns two separate claims: blow-up for ordinary Navier–Stokes with smooth forcing, and blow-up for unforced Euler from smooth initial data. The first, if verified under the stated hypotheses, would establish an allowed breakdown alternative in the Millennium Problem formulation. It is distinct from unforced Navier–Stokes blow-up. At this moment we are not in a position to say anything substantive about a comparison between OpenAI’s constructions and our cascade methods. Assessing the announced proofs and their relationship to earlier work requires a detailed mathematical analysis.

The cascade leaves us with concrete mathematical questions. Which geometric features and cancellations let one layer amplify the next while controlling the full nonlinear interactions? How do they determine the regularity attainable for the force, and which parts of the mechanism survive stronger dissipation? Its application to several incompressible models gives us a way to investigate these questions within regimes of classical local existence.

[This is a guest post by Jennifer Taback. This blog post was initially written in a different file format and converted using AI. — T.]

Recently I have read a stream of articles questioning the future of mathematics: what constitutes a proof, what we value, how we retain the human enterprise of creating knowledge. Many of these articles are written by mathematicians making significant progress on the conjectures that shape their fields, whose work is now imperiled by the capabilities of frontier AI models. I am not one of those mathematicians. There are many mathematical problems that I have revisited over two decades, but none will grab headlines. Nevertheless, I care deeply about their resolution, as do others in my field. What does the advent of powerful AI models mean for mathematicians like me? I have yet to succeed in prompting a solution to one of my long-term problems, though AI models have helped fix an incorrect lemma and suggested a helpful reorganization of a paper. They have pointed me in directions in which I had not thought to look, and spurred me to learn new mathematics. Combining AI with the skills I have honed over the years is making me a stronger mathematician.

Journals prohibit AI models as co-authors, but these models have proven to be effective partners for me. I teach at Bowdoin College, a selective liberal arts college in Brunswick, Maine. While I have many wonderful collaborators, none are local. At my college, I have no one down the hall with whom to discuss research questions; mathematics departments at small colleges rarely have two colleagues in the same specialty. AI fills this gap for me. I respond to its (not always correct) answers to my questions, and ask for clarification as I would from a human collaborator. AI makes me ask myself more probing questions, challenging me to dig deeper into my accumulated knowledge and connect it to the broad synthesis the model can often provide. And sometimes AI is just wrong or confusing, as a human might be, and I move on.

Mathematics is a human endeavor, and machine-generated output requires substantial human intervention in order to contribute to our knowledge base. Having co-organized two conferences on “Communicating Mathematics,” I know that every idea that advances mathematics, whether human- or AI-inspired, requires clear exposition, a skill most of us could improve. AI is helping me here as well; it is making my mathematical writing better by catching small inconsistencies in papers I believed I had diligently proofread, and helping me sharpen my arguments. Our profession should embrace responsible use of these tools in the service of stronger communication.

AI has arrived in my classroom too, at an institution that demands pedagogical excellence and innovation alongside active research. I expect my classroom to change more in the next two years than it has in the previous twenty, in unknown and unexpected ways. I am angry at AI for forcing evaluation into the classroom under timed conditions. I do not perform my best under those circumstances and neither do my students; we have narrowed assessment to what we can proctor. Without graduate student assistance, thoughtful oral examinations, for example, are impractical at the scale of my teaching. Faculty at small colleges, even well-endowed ones, rarely have the graduate students and teaching assistants that make such solutions feasible.

Conversations addressing pedagogical changes resulting from widespread access to AI models are proliferating, but they are often convened at R1 institutions. These conversations must be broadened to include faculty from the entire spectrum of colleges and universities, especially those with higher teaching loads and more limited support. I am optimistic that by working across institutions we can strengthen undergraduate mathematics education. Students will influence this work as well; some of my undergraduates have been remarkably creative in their use of AI tools to further their understanding. One student in my cryptography class, for example, built an animation of a WWII-era encryption device that let viewers watch the mechanics and the mathematics unfold together. I have no overarching answers yet. But I want my students to trade their fear of being replaced by machines for the excitement of building what comes next.

I write this with the security of a tenured professor. In a small department where mentoring is a personal responsibility, I hear the visceral worries of my junior colleagues who are unsure of their path to tenure and beyond. Their position is genuinely different from mine, and their promotion equally weighs research and teaching. They are building a record under rules that do not yet exist.

Working toward new standards for the discipline is not an abstract matter. We have to decide what counts as proof, and what we value for publication and tenure. I would like us to disclose the tools we use for research without fear of judgment, while taking personal responsibility for ensuring that our work is rigorously verified, understood, and explained before we disseminate it. We should not abandon lines of inquiry for fear that AI will get there first; second proofs of theorems, whether by humans or by AI, often provide valuable insight into a problem. I do not want to surrender my questions, nor would I want my junior colleagues to cede theirs.

If we do things differently, adopt novel technologies, and investigate new frontiers of the discipline, we will still be producing mathematics. I love what I do, and I feel I am doing it better than ever. I will keep learning and seeking understanding while making the best use of the resources available to me. I do not know what mathematics will look like a decade from now. I know it will be created by people who have learned to ask insightful questions, and I know we are the ones who will teach them to do that, both in liberal arts classrooms and at research universities. Mathematicians will continue the hard work of discovery and understanding using stronger, and perhaps stranger, tools, pursuing problems yet to be posed.

Just a quick post to note that the International Council for Industrial and Applied Mathematics (ICIAM) has released a statement on mathematics and artificial intelligence (as well as a longer version), which makes many points echoing several already made recently here and elsewhere.

The longer statement also makes reference to a recent statement by the London Mathematical Society on recent developments around the Navier-Stokes equation. Perhaps the comments to this post can also be used to report other institutional statements on these topics.

[This is a guest post by Bryna Kra and Rachel Ward. -T.]

The Summit on PhD Math Education in the Age of AI was held September 17–18, 2026, jointly hosted by the Harvard Department of Mathematics and the Center of Mathematical Sciences and Applications (CMSA). It brought together twenty-four senior mathematicians from across the discipline, along with several current PhD students and postdocs, to examine which aspects of the mathematics PhD need rethinking as AI reshapes thinking-based work.

This document is a first draft of our recommendations; we expect to refine our recommendations over the coming months according to changing landscapes and your feedback.  We encourage feedback in the form of comments on this post, or by sending email to education-summit@cmsa.fas.harvard.edu.

To graduate students and early-career mathematicians: We know this uncertainty is weighing heavily on you as you plan your next steps. Your concerns matter, and we want to hear them. We are gathering information, keeping communication open, and working to support your opportunities and your future in mathematics.

[This is a guest post by Amit Sahai. This blog post was initially written in a different file format and converted using AI. — T.]

When I was an undergraduate student, I remember talking with several students who felt that the pace at which the top students could understand new math concepts was far too fast for them. They, too, could understand the ideas, but it would take them much longer. Eventually, almost all of these students gave up their dream of pursuing research mathematics and found something else to do. I have been thinking about those students a lot in the last few days.

The research mathematics community consists largely of those of us who either rarely felt that way, or who felt it and managed to overcome it through hard work. We have had the good fortune to find a place in mathematics where we could make progress. But we are now entering a time for humility: a time when all of us are going to know what it feels like to be unable to keep up.

The AI systems I have worked with are already producing beautiful new ideas. They are doing far more than impressive calculations or quickly carrying out arguments that a strong human researcher would already understand. And we probably can’t even imagine the wonderful ideas that future systems will be capable of producing.

When we feel that we cannot keep up, will we take that as a reason to leave research mathematics, like the students I am remembering? As more of us experience this, there will undoubtedly be a temptation to draw the same conclusion as they did: If the machines can move so much faster than us, perhaps we should find something else to do.

For our community to give up the work of understanding would be a profound abdication of our responsibility to humanity. Each of us is entitled to choose a different life. The responsibility I am talking about belongs to us collectively: to build a future in which humans can understand and contribute to the discoveries that will change our world. A future with meaningful human agency.

Struggle is essential to understanding difficult concepts. Fortunately, this struggle can be shared. I have been blessed to experience this time and time again with my students and collaborators. Imagine a multitude of research groups, each with sustained support, each spending a term or a year trying to understand an extraordinary set of ideas produced by an AI system, with the help of AI systems. [1]

This may very well be among the most important mathematical work in the years to come, and we should support and prioritize it accordingly. This enterprise will require a significant expansion in the number of mathematically sophisticated human researchers available world-wide, as major breakthrough ideas accumulate.

Why should society want this? So far, this might sound like a utopian fantasy for us – a civilization focused on depth of human understanding, awash with mathematicians and physicists and the like. I would certainly love to live in such a world. And indeed there are deep philosophical reasons for society to move in this direction. But I think society has a much more immediate stake in making this possible, too.

Imagine that a future AI system proposes a radically new design for a one terawatt nuclear fusion power plant. It has found a way to sustain and control fusion that no human had conceived of. The design promises abundant, inexpensive, clean electricity. Robots stand ready to manufacture the components and build the plant.

A terawatt is an insane amount of electrical power. We would be deciding whether to construct a machine that handles extraordinary flows of energy using principles we have never conceived of, let alone put into practice. We would need to understand how failures can be contained, what happens to energy already stored in the system when it shuts down, how we can be sure that the materials that make up the power plant behave as expected, and what other questions we should ask before proceeding. The very novelty that makes the proposal exciting would mean that we cannot inherit confidence from decades of operating similar plants or experiments.

Before approving construction, I would want communities of humans to understand why the design works and what justifies confidence in its safety. I would hope that we all would.

Human involvement does not automatically improve a technical decision , and I see no reason to insist that humans manually repeat work an AI system might be able to perform more reliably, even including proving mathematical guarantees. But a theorem can only exist within a model. Understanding the guarantee means understanding the model, the experimental evidence for it, and our uncertainties about the accuracy of the model. This is demanding work, and mathematically sophisticated people must be available to engage with it.

One might respond that AI systems should handle those questions too, and ultimately decide whether the plant should be built. That is a serious position. But it asks us to accept a future in which decisions of enormous consequence rest on reasons that no human community understands.

I do not want us to arrive at that future simply because we failed to invest in our own capacity to understand. Human agency is a value of fundamental importance. We must retain the ability to meaningfully consider alternatives and decide what kind of world we want to be a part of building. I think it is worth the effort. [2]

To take on this responsibility, we may need to broaden our view of what a mathematician can contribute. I have in mind something like a “deployable intellectual reserve”: communities of mathematically sophisticated people that humanity can call upon to help understand consequential AI-enabled breakthroughs.

Our ability to understand difficult and unfamiliar ideas may become one of the most important contributions we can offer to society. We should be willing to bring that skill to problems far beyond our usual research interests. [3] Doing so asks us to expand our sense of our vocation.

A counter-argument might be that AI systems will make each of us so much more effective that fewer people could do this work, even as the pace of discovery accelerates. But each of us is merely human. We have fundamental limitations based on our biology. Depth of understanding needs time and a pace of life that humans can sustain. Each individual human can only be asked to do so much, but through earnest cooperation we can accomplish much more.

If AI fulfills its promise, we will encounter more beautiful and consequential ideas than we have ever seen. We must respond by building thriving human communities that can understand them together.

We’re gonna need a lot more mathematicians.

The ideas and opinions presented here are entirely my own, but GPT 6 Astra was instrumental in helping me draft this note. I also thank my former student Dakshita Khurana, my current student Isaac Hair, my colleague Terence Tao, and my family members Anant Sahai and Gireeja Ranade for valuable feedback. Note that there is much more to be said here, but I tried to keep this relatively short to focus succinctly on my primary thoughts.

Notes

[1] By this, I do not mean to imply that only AI-created results will be of interest in the future. But for major results generated by humans, we already have a tradition of spending extended periods of time studying them.

[2] And the relevant understanding cannot belong only to the organization proposing the technology. Imagine a public hearing at which the company’s experts are the only people capable of following the technical argument. Independent expertise is critical.

[3] Indeed, AI systems are likely to be very helpful in allowing researchers with diverse backgrounds to talk effectively with one another, and more generally understand unfamiliar concepts.

[This is a guest post by Tapio Schneider. This blog post was initially written in a different file format and converted using AI. — T.]

[This will be cross-posted on the CliMA blog.]

The apparent proof of finite-time blow-up of the forced Navier-Stokes equation, announced by OpenAI on September 8, has brought into focus a debate about the role of AI in mathematics. The proof was produced with a system of some 10,000 AI agents that explored many approaches in parallel; it was then formalized and verified in Lean. The formal verification supports its correctness, but mathematicians are still working to digest it. A proof settles the truth value of a statement, but Terry Tao and others have argued that this is only part of the point of proofs; the other part is to advance our conceptual understanding of “basic structures of shapes, numbers, and natural phenomena.” As Yehuda Rav put it a quarter-century ago, “theorems are the headlines, proofs are the inside story.” A proof that is correct but incomprehensible, or undigested by the mathematical community, gives us the headline without the story. The issue is not whether the prover is a human or a machine, but whether the reasoning advances our collective understanding of methods and structures, which can spur new thinking and further advances. As Timothy Gowers has noted, the inadequate AI-generated write-ups of proofs are likely a temporary annoyance.

I want to argue that the same point about understanding holds in the natural sciences and engineering, where it also has intrinsic value and, in addition, acquires instrumental value when predictions must be trusted before they can be verified empirically. One role of science is what ancient philosophers called episteme, roughly explanatory understanding; here, understanding is the goal itself. Another role is techne, roughly the craft of predicting and making: forecasting how natural or engineered systems will behave under circumstances not yet observed. Whether the two roles can be separated depends on how easily predictions can be checked. When they can, techne can stand on its own. A black-box AI weather prediction model can predict tomorrow’s weather, and we can trust it because its forecasts can be checked every day. Techne can then also serve episteme as an instrument. For example, AlphaFold predicts 3D protein structures without providing explanations. But its predictions can be checked against experimentally determined structures, and they have become invaluable for understanding how drugs bind to their targets. Episteme and techne become inseparable when predictions must be acted upon, and hence trusted, before they can be empirically verified, because verification is too slow, costly, or dangerous, as in projecting climate change decades ahead or designing an aircraft. In those cases, an auditable causal chain from assumptions and input data to the predicted outcomes is what makes predictions trustworthy, and this constrains how AI can be used.

The Navier-Stokes equation, which describes fluid flow, is a good example, as it is at the heart not only of a Millennium Prize problem but also of aircraft design and climate prediction. The claimed result says that a fluid starting from rest, driven by just the right smooth stirring, develops an infinite velocity spike in finite time while its total kinetic energy remains bounded; the forcing is constructed to sustain the collapse. (The unforced version of the problem, whether smooth solutions exist for all time without external forcing, remains open.) Despite the mathematical singularity, nothing infinite happens physically: the incompressible equation stops being valid once energy concentrates at very small scales, where compressibility and molecular effects take over, as has long been known. By contrast, in turbulence, viscosity dissipates energy at a small but finite scale (the Kolmogorov scale), and the continuum description is valid across all scales of motions. Therefore, the result says little about how we model, predict, and understand the physical phenomenon of turbulence, which is likewise a solution of the Navier-Stokes equation, and one that, unlike finite-time blow-up, is ubiquitously realized.

The Navier-Stokes equation governs the flow and turbulence that control lift and drag around an aircraft wing, cloud formation in the atmosphere, and mixing in the oceans. In both aircraft design and climate prediction, verification comes late or is difficult and expensive. An aircraft is flight-tested only after it is built; a projection of how extreme rainfall statistics intensify in the coming decades must inform stormwater infrastructure that is built now but will likely be put to the extreme test only decades later. Such predictions earn trust not by end-to-end verification but by being the output of an auditable chain stretching from inputs (design parameters, atmospheric composition) to outcomes, whose links have known limits of validity and can be tested individually. Computational fluid dynamics (CFD) solves the Navier-Stokes equation together with additional equations (e.g., for thermodynamics) numerically. Its numerical methods for the resolved scales are based on established theories of stability, consistency, and convergence, and its subgrid-scale models for unresolved turbulence rest on plausible assumptions of universality at small scales (e.g., local isotropy) that can be tested separately against high-resolution simulations or laboratory experiments with canonical flows. Understanding and auditability of the individual links are what allow the chain as a whole to be trusted beyond the distribution of large-scale cases already observed, such as the present climate or existing aircraft wing designs.

Contrast that with end-to-end AI methods for weather prediction. Daily empirical verifiability suffices to establish trust in their forecasts. However, they do not come with a stability, consistency, and convergence theory (no analog of von Neumann stability analysis or the Lax equivalence theorem has been established for them), and how an initial condition becomes a forecast is difficult to audit. This is inconsequential for forecasting a few days ahead, where the forecasts can be checked daily. But it does matter for climate projection, which is a different task: predicting how weather statistics change over decades in response to a forcing such as increased greenhouse gas concentrations. An end-to-end model can learn the day-to-day evolution of weather states in today’s climate, but it contains no pathway through which greenhouse gases alter this evolution; their concentrations are typically not among its inputs, and if they were, no observations exist to learn about the response. The causal chain from greenhouse gases to their effects on radiative transfer, temperature, and winds, represented in physics-based models through their equations, is absent. Additionally, such models do not enforce conservation laws, for example of energy, so long integrations can drift by accumulating errors (e.g., in temperature). We would not currently trust them to project how the climate system responds to previously unobserved changes in the concentration of greenhouse gases over decades. Nor would we trust an AI surrogate of CFD simulations to certify an aircraft of novel shape. AI surrogates are used to explore and narrow down design spaces quickly, but the final assessment returns to established CFD methods or wind tunnel experiments, whose errors are controlled and whose steps are auditable.

So how do we best use AI in cases where episteme and techne combine, where understanding is essential for trust because predictions are difficult to verify? An answer suggested by the preceding argument is to embed AI at the links in the chain where trust can be earned by empirical verification. Concretely, use AI inside auditable scaffolds, such as physical conservation laws. Then use numerical methods with controlled errors to solve, e.g., the Navier-Stokes equation on the resolved large scales, while learning closure models for the unresolved subgrid scales from data, where some universality assumptions are defensible and individually testable. The rationale, in the case of the climate system, is that the large scales are where climate change moves the system out of the current distribution, whereas small-scale physics obeys the same local laws in a warmer or colder climate as in today’s. For an aircraft wing of novel shape, similarly, the geometry may be new but the functional relation between larger-scale conditions and the small-scale turbulence around it is not. The scaffold thus guides the extrapolation on the basis of the known equations, rather than with end-to-end models tied to the data available today.

Closures must be learned as functions of the resolved state, and extrapolation problems may reappear if the conditions for which data are available do not span the range of conditions for which predictions are needed (e.g., the temperature and humidity regimes in which cloud turbulence has been sampled, or the pressure gradients along a wing of novel shape). This can be mitigated with established tools, such as local high-resolution simulations for offline calibration and uncertainty quantification. Climate models and CFD codes have been built from resolved dynamics with embedded closures for decades. AI now enables a wider and faster search. Neural network closures can be individually tested and, to some extent, interpreted. Symbolic regression, which learns equations by selecting terms from a dictionary, as in SINDy, can sometimes produce closures that are more easily interpretable. AI agents are beginning to run the closure search in a closed loop, proposing symbolic closures, testing them against high-resolution simulations, observations, or experiments, and revising them. When this is successful, the resulting closure can be audited and, after the fact, understood.

This closed loop is similar to how AI is used in mathematics. In both cases, a verifier is used for checking: Lean for proofs; high-resolution simulations, observations, or experiments for turbulence closures. In the case of mathematics, the checks are complete; in the case of turbulence closures, they are limited to the conditions covered, so trust is restricted to the tested conditions. AI can accelerate this program by searching a larger space of possible closures or proof strategies than can be explored by humans in the same time. Once candidates have passed the checks, they become new objects for human study. In this way, understanding (episteme) and prediction (techne) improve together and reinforce each other, with humans, for now, remaining essential for extracting understanding and building trust in the end result: for writing the story behind the headline.

I thank Thomas Müller for pointing me to the paper by Yehuda Rav, and Thomas and my CliMA colleagues for discussions of the topics here over several years. I used AI for copy-editing.

[This is a guest post by Martin Hairer, cross-posted from Proofs and Prompts. — T.]

There has been a lot of speculation regarding the “Advisory Group on Mathematics and Artifical Intelligence” agmai.org since it was announced on Monday. In this short blog post, I would like to explain in a bit more detail how the group works, what we are trying to achieve, and why I agreed to be part of this group.

First of all, let me lay down some facts that seem to have been drowned in a torrent of misinformation. The most important one is that we are genuinely independent of OpenAI and any other of the so-called `frontier’ AI labs. Yes, the original impetus of forming this group was OpenAI’s response to the statement A Severe Misalignment of AI in Mathematics, but not all members of the group were contacted by OpenAI in the first place, there is nobody besides the nine of us taking part in our conversations, we do not receive any monetary compensation, and our technical support (so far mainly regarding IT, legal, and communications) is being provided by the IAS. We also have not signed any documents placing any constraints whatsoever on what we state in public and whose advice we seek, besides the obvious confidentiality requirements. The other fundamental fact is that our overarching aim is to represent as well as we possibly can the interests of the mathematical community. This is a tall order and we may end up doing a terrible job at it (I certainly hope not!), but I am absolutely certain that all nine of us take this extremely seriously and are acting in good faith.

I am acutely aware of many of the pitfalls of being part of such a group. At a most basic level, the mathematics community consists of people with a very broad range of views and opinions (often strongly held ones!), and the nine of us clearly don’t form a representative sample. As an independent body our role is purely advisory, so the AI labs can choose to simply ignore it. It would also be very naïve to believe that the AI labs won’t try to spin whatever we say in a way that suits their PR machine, which dwarfs anything we could possibly come up with. Finally, given that the unprecedented situation we find ourselves in has the potential of impacting the lives of so many people (I intentionally do not use the word `career’ since for many of us mathematics is so much more than just a career), whatever statement we make and / or advice we give will necessarily upset a sizable fraction of the maths community. So why on earth would I accept to be part of this?

Here are some of the reasons that swayed my mind:

1. The recent releases, on privately controlled websites, of high-profile mathematical results combined with abject levels of scholarship and only minimal presentation effort has been undermining the usual standards of scientific practice. If we refuse to answer when being asked how to do better (irrespective of whether that ask is being done in good faith), how could we then complain about this behaviour?

2. It is obvious that AI has already had a profound impact on mathematical research and raises numerous questions of correct attribution of ideas, priority, human understanding of ideas, etc. Many aspects of this revolution will be addressed within our community, but it makes no sense of taking a hard `ostrich’ approach of simply ignoring the AI labs and refusing to talk to them on principle.

3. It is perfectly legitimate to question OpenAI’s motivations, but the fact is that they have now made an effort (as belated and minimal as it is) to engage with the mathematical community. Turning them down without even trying to engage with them would be the easiest way for them to get a PR win painting the mathematical community as a bunch of out of touch luddites.

4. In the `Severe Misalignment’ statement, which has now been endorsed by nearly 8000 mathematicians, we conclude by saying that “These issues must be addressed urgently, in the mathematical community, by the companies developing these technologies, […]”. It would be rather hypocritical of myself to then chicken out at the first opportunity of actually having a chance of setting up some form of communications channel between the mathematical community and the AI labs just because I could get some flack for it.

Regarding the actual advice we intend to provide, it is a fact that AI companies have in recent months been producing some high profile mathematical results and that their publication and dissemination has been falling far short of acceptable mathematical practice, whichever way that is defined. However, the situation at hand is sufficiently unprecedented that we genuinely haven’t completely made up our minds yet on the best way forward and we fully intend to gather as much feedback as possible, be it through our feedback form, discussions with colleagues, the discussions on this blog, etc. We are going through a period of intense turmoil (and this doesn’t just concern mathematics) but I am heartened by the many intense but thoughtful and respectful discussions I have experienced both inside my own institution and at gatherings of mathematicians like the ICM over the past few months. I am convinced that the mathematical community can emerge all the more united and stronger from this experience.

[This is a guest post by Antonio Auffinger. This blog post was initially written in a different file format and converted using AI. — T.]

Despite writing papers in pure mathematics, much of my time in the past decade was spent talking (mostly listening, to be accurate) to biologists, computer scientists, and physicists. Theoretical physics and computer science are grounded in mathematics and thus share much of our language and, to some extent, our culture. The barriers between biology and mathematics are an order of magnitude higher. I am convinced that biologists are part of a different species. The language, incentives, culture, training, and everything else you might think of appear to be completely disconnected from the way we do mathematics. Yet, the similarities are abundant: the pursuit of understanding, the excitement of discovery when new patterns or phenomena emerge, and the hours needed to make minor advances, sometimes leaving us with just frustration. The intuition of setting up a new experiment feels like witchcraft to me, much like our way of finding connections between different abstract objects feels like magic to them.

What does talking to biologists have to do with the future of mathematics?

It could be beneficial to look at what is happening and what has happened with our neighbors, even if none of us can predict where we will be two years (or even three months) from now. A first lesson that I learned is that a large part of biology is technology-driven. Fields completely change, emerge, and die in a matter of years. The advent of CRISPR, RNA-seq, and cryo-EM, for instance, suddenly allowed humans to observe and manipulate phenomena that were previously inaccessible. These tools generate precious data, and the incentives often favor a culture of seclusion, where discoveries are frequently not shared until the final product is complete.

This has made me appreciate the culture of mathematics. Mathematics has never been free of competition or secrecy, but we abundantly share. We share ideas, we share problems, and we share entire skeletons of approaches with our colleagues, with visitors we just met, in talks, in public forums, and on YouTube. I suspect the enormous effort often needed to produce a proof, even with a full outline, has helped sustain this openness. Mathematicians and mathematics have deeply benefited from this open attitude. Many new connections and major discoveries have started with honest conversations at coffee breaks, in hallways, or on hiking trails. Sharing ideas or arguments before they are fully formed allows others to see pathways we missed, point out obstacles, or take the problem in directions we had not imagined. Also, it is simply more fun to do math together.

My worry is that this unselfish openness will become a thing of the past. If proof generation becomes a fast, accessible commodity while our ways of giving credit remain unchanged, mathematicians (especially those still building their careers) may feel encouraged to optimize locally in ways that weaken our culture of sharing. In the past few weeks, I have had colleagues reach out for advice and tell me they will no longer post on arXiv. I have witnessed trainees posting rushed papers online for fear that others could quickly carry out strategies already outlined in previous work. I am also part of the problem, as I have started advising my students to be extra careful when sharing work in progress.

Biology also offers examples of communities deliberately changing these incentives. During the Human Genome Project, the Bermuda Principles called for the rapid public release of sequence data. Later, the Fort Lauderdale Agreement tried to balance this openness with proper recognition of those generating the data, placing responsibilities not only on researchers producing and using the data but also on funding agencies. Although it is focused on data, it is an example where the status quo was changed by community intervention.

I do not know what the right analogue is for mathematics, but I believe we need to start thinking about it. I encourage the community to reshape our incentives and the way we give credit, to ensure broad accessibility to these new tools, and to make openness a reasonable choice, especially for those still building their careers. Senior mathematicians must engage in serious conversations about ethical use with their trainees. In turn, trainees should be encouraged to truly explore, because many of the solutions to the issues we currently face as a community will come from them.

None of this is an argument against the use of AI in mathematics. I believe these tools will raise the ceiling of the things we can discover, leading mathematicians to ask new questions and understand new phenomena.

This brings me to the second lesson I learned from my biology colleagues: many of the questions I hear from biologists need mathematics. New mathematics. There is room here for topologists, number theorists, dynamicists, algebraic geometers, analysts, etc. This is not just because of our capacity as proof builders, but also because of our capacity for abstraction and for understanding phenomena. Applied sciences are generating complex, time-dependent data that require new methods and theories. This is also a two-way street. Decades ago, topology and knot theory unexpectedly provided a framework for understanding how enzymes untangle and rearrange DNA. In the other direction, attempts to understand population genetics and how gene frequencies drift over time helped motivate new classes of infinite-dimensional stochastic processes, including measure-valued diffusions. Today, geometry and probability underlie dimension reduction methods that biologists use daily to make sense of massive single-cell datasets, such as t-SNE and UMAP.

I am not suggesting that mathematicians need to pivot to biology or any applied science. The pursuit of mathematics for its own sake is the absolute bedrock of our field and that must remain intact. However, as AI changes the landscape, looking outward presents an incredible opportunity to discover new questions, new phenomena and new mathematics, and perhaps AI might even lower the barriers to taking that leap.

Mathematics has much to offer the other sciences, and much to learn from them. I am looking forward to what comes next. Proofs may increasingly be generated by machines, but the ultimate purpose of mathematics remains exactly what it has always been: to ask questions and to understand.

[This is a guest post by the Advisory Group on Mathematics and Artificial Intelligence. This blog post was initially written in a different file format and converted using AI. — T.]

We would like to use this guest post to announce the creation of the Advisory Group on Mathematics and Artificial Intelligence hosted at the Institute for Advanced Study (Princeton) and online at agmai.org.

The rapid advances in artificial intelligence (AI) present both opportunities and challenges for mathematical research. We believe that we are at a historic moment for our discipline. Recent events raise urgent questions about how to support the long-term prospects for deep human understanding of mathematics.

Purpose. The purpose of this group is to advise AI companies on their interactions with mathematical research and with the mathematical community, including the responsible presentation and release of mathematical results. We seek to work for the best interest of mathematics and the mathematical community, and to serve as one possible channel of communication between mathematicians and the AI industry.

Independence, Transparency, and Accountability. This group operates independently of any AI company and members do not accept payment for this work. We will publish our recommendations to AI companies on this website. We are willing to offer such recommendations to any AI company whose models are likely to have a significant impact on mathematics. Although we will give advice, we do not have decision making power at any AI company, and the responsibility for the decisions made by any company will rest with that company.

Advisory Group Members

• François Charles (ENS-PSL)
• Camillo De Lellis (IAS, GSSI)
• Timothy Gowers (College de France, Cambridge)
• Martin Hairer (EPFL, Imperial College London)
• Nikhil Srivastava (Berkeley, Simons Institute)
• Ulrike Tillmann (Oxford, INI)
• Ravi Vakil (Stanford)
• Edward Witten (IAS)
• Melanie Matchett Wood (Harvard)

This group came together after OpenAI approached some of its members about establishing an external advisory board. In agreement with OpenAI, they decided to create an independent group and invite others to join.

Current Task. We are currently facing the very specific challenge of advising OpenAI on how to coordinate the release of a large number of significant results in mathematics that they report have been produced by their internal model.

We welcome input from the mathematical community on this question. Please use this form to share your thoughts with us as soon as possible. Your responses will be used to inform our recommendations and will not be made public without your approval.