AI, Lean, and sharing mathematics

AI, Lean, and sharing mathematics

Over the last few months I have gotten back into Lean and worked with LLMs to formalise much of my own mathematics as well as the mathematics that I rely on. A concrete result of those is a GitHub repository for Fractal Geometry that may be interesting to you if you want to formalise similar results. A link can be found at the end of this post, which is all about recent happenings in AI and Maths.

The Drop. On 6 October 2026, OpenAI released a collection of PDF documents and proof artifacts produced by an internal model, including Lean formalisations of many of the purported proofs.

The October release claimed major advances across many different fields and has forced mathematical communities to reconsider how we do mathematics. I regard the release as grossly irresponsible academic conduct. Releasing an avalanche of badly written articles with bold claims leaves the community to sort through them, repair exposition, and reconstruct missing context, in addition to checking correctness. I am especially concerned about the harm to young researchers whose projects and prospects have been upended, and to the trust and cooperation on which the field depends, both between AI companies and amongst mathematicians themselves. It has accelerated scooping and unethical behaviour, and made mathematicians reluctant to discuss ideas openly for fear that someone will push a button and claim the results. For someone established this may not be too harmful, but it is an absolute disaster for early career mathematicians.

OpenAI say they consulted the independent Advisory Group on Mathematics and Artificial Intelligence, but ignored almost all their recommendations and failed to engage responsibly with the affected communities. The documents released did not constitute (as a whole) scientific articles as they fail academic practices, do not give credit to where their ideas came from, and were simply released in a GitHub repository with no human review or quality assessment. The advisory group’s response also made clear that they did not endorse the process by which the results were obtained. There are also serious concerns about the possible use of researchers’ private work without permission, as Andreas Thom has described.

In the uncertain future of mathematics, I believe that it will be necessary for us to reevaluate how we judge people and their mathematics, not least to judge how resources are divided. When parts of mathematics can become automated, we must still recognise the value in actual human understanding and the ability to explain and educate this understanding. But how to do that is left to another post.

My own use of AI: Lean No matter one’s opinion on the OpenAI drop, I think most mathematicians agree that the use of LLMs has become very disruptive. Several journals have stopped accepting new submissions until a robust response can be found. Personally, I experimented a lot with LLMs over the last year, but had very limited success in “training the slop cannon” to output reasonable mathematics. However, I did realise around April 2026 that it is an effective tool in something I have long been trying to do: formalise my own mathematics.

My journey with Lean as a formal proof checker started in 2022, when I went through all the brilliant resources available then. In particular Mathematics in Lean was a great resource to start with. However, one of the problems with formalisations had been the slow progress. Given its very nature, Lean is highly syntax sensitive and writing proofs of anything I considered research-level was well beyond my ability and patience. The advent of agentic AI changed things for me. Talking LLMs through the proofs allowed me to formalise research-level results in just a few weeks, although I would not claim that the resulting Lean code is well written.

But here also some prudence is required. Given that Lean is a computer language, it has bugs. And LLMs have become very good at exploting these bugs to write Lean code that compiles, but is no proof! See for example the exploit used in “disproving” the Collatz conjecture, described by Leonardo de Moura. To combat this behaviour, one needs to be able to read at least some Lean and use ‘proper’ set ups that minimise the risk of problems ocurring. One of these is the Comparator. It reduces the task of verifying the Lean formalisation to humanly checking a Challenge.lean file for each formalisation. This contains the statements to be proved, the definitions needed to read them, and any assumptions taken from the literature. The proofs are kept separately and checked against these statements. Reading the challenge lets one check that the formalisation actually says what one intends it to say: a formally correct proof is only useful if we have stated the right result and that there are no alterations of that statement hidden deep in the Lean code (which is what Comparator checks).

I have since continued trying to formalise all my results, and so far the following have appeared on Palomar:

I also formalised a substantial part of my geometric measure theory course in its course library. The library includes definitions of several notions of dimension, covering arguments, Frostman’s lemma, and similar results. Some of the article formalisations rely on literature results that I have not yet managed to formalise due to lack of time and tokens, but I started to build a library for fractal geometry.

Fractal Geometry Lean Library. This library is now available on my GitHub account here. It contains an ever growing list of results in fractal geometry and related areas, and in the interest of open science, I can only encourage their reuse for your own projects. Some of these may appear in a more polished form on Tau Ceti, and possibly, down the road, in Mathlib. While many of the proofs are AI written, making these developments public and discoverable will hopefully reduce some ’re-proving’ necessary for researchers in similar areas.

That is one sense in which I would like this use of AI to become sustainable. The time and resources spent on a project should leave something useful for others: accessible statements, documented dependencies, proofs that can be checked again, and code that can be built upon. Registries such as Palomar help make formalised results discoverable and record exactly which version was checked. Keeping the libraries useful will also take shared work on documentation, maintenance, and connections between different developments.

If you would like to use the libraries, contribute a result, improve the documentation, or connect this work with your own formalisation projects, I would be happy to hear from you. The repositories are open, and I would like them to become useful for people working on fractal geometry and related subjects and grow in completeness so one can consider adding them to bigger repositories.

Hopefully we can, as a community, find a way again to give value to intellectual, sustainable, and helpful work.