After they announced the formalization of the classification of Finite Simple Groups, I immediately wondered "What would happen if you tried to formalize the Stacks Project?" Despite also being very long, it's the opposite of the CFSG: instead of a poorly organized set of results that contribute to proving one big theorem, it's instead a carefully-organized set of results that cover a broad area.
The Stacks Project was the model for how mathematics should be done (at least for the pre-LLM era). Algebraic geometry had lots of poorly organized foundational results that were not really created for themselves, but in order to solve problems in the field. One person, Aise Johan de Jong, set out to fix it by organizing a project to write out the proofs of all of the results in a carefully organized fashion. He's led the project since, though of course there are multiple contributors. The whole thing is thousands of pages.
I would be interested in hearing more about the gaps they uncovered in the existing results, and how they fixed them.
I actually believe that this isn't the way to go when proof is cheap. Due to the straitjackets of type theory sharing proofs across domains is painful for most human readers to consume. With AI it's much easier to specialize theories. It's just not worth the cognitive cost to build on top of broad and shallow theories. To have any hope in keeping up with AI we need to instead better appeal to the largest component of our brain - namely our visual cortex.
Okay this is actually useful AI formalization. But the stacks project is basically Lean in natural language anyways, so it makes sense why its high quality.
Kind of ironic that (as of today) the most recent blog post from Oct 21 '26 on the original Stacks Project is "21 Oct 2026: No AI for now"
A very good friend of mine is an algebraic geometer and all of the AI progress in math is, to put it mildly, bumming him out. And me too honestly!
I understand the allure of doing this kind of work in AI on some level, but I'm becoming increasingly skeptical of generating "knowledge" that's difficult or impossible for humans to understand (at scale or otherwise).
The one bottleneck in this new AI era of math is still human understanding. No matter how much new stuff you can prove, to understand something you still have to basically do stuff the old fashioned way. Maybe AI can help a little, but without working through problems and proofs, you still won't get much farther. Ultimately our minds are limited that way.
I tend to think that the progress of mathematics before AI was roughly suited to the way humans assimilated understanding, but now with AI, the progress in mathematics is going to go much faster, oustripping our ability to understand it.
It is true that more mathematicians could theoretically eventually go through it, but the process of progress itself is discouraging and thus paradoxically renders this new AI era of math much less interesting to many.
I guarantee that after the intial "look at all the stuff we can prove", the benefits of using AI will dwindle rapidly.
Yes, "This milestone begins with the Stacks Project itself". Could half AI slop effects be mitigated by a prompt "Don't mix or mangle metaphors here"? A milestone is a step in a process, not the entire process.
Once this kind of sloppy effort to sound impressive was just "over writing" but its now a strong tell for AI.
Why is that a mixed metaphor? I'm very used to large initiatives/programs with several large milestones, each involving multiple projects. I don't see any issue with it.
The milestone they are reaching is the formalization of The Stacks Project. It began whenever they started prompting an AI to do that or started preplanning.
The metaphor of milestone is a goal reached within a larger process. I think that, yeah many people will not find a problem instances of this sort of (mis imo) usage but AIs to create a sequence of these things and that tends to create a tone to AI writing that many people can feel even if they can't point to particular problem usage.
Axiom raises $264M, publishes this massive lean proof built with AI, and you're moaning about some AI language in their description. AI is in their domain name. What are you doing?
And here's another example of mangled word use: "creating a sweeping dictionary between algebra and geometry that allowed mathematicians to do geometry over arbitrary rings, with arithmetic and infinitesimal data built in from the start."
What does "sweeping dictionary" mean?! And I don't think "creating ... across" is the right to way to construct indirect objects. In old writing day I think it would be called an "awkward construction" but I everyone's very used to such awkward constructions AI tells.
Consider they/it could have said "creating a link between algebra and geometry that allowed mathematicians to do geometry over arbitrary rings, with arithmetic and infinitesimal data built in from the start. ", in fact that's the language I'm used to.
It's shame because twisting metaphors in an ad-hoc way can be a nice thing but LLMs do this constantly and badly and mother looks at the (simulated) kids and says "this is why we can't have nice things".
Edit: I can't help myself "...In a tightly interconnected dependency graph of definitions and theorems..."
Sure, connected and interconnected mean nearly the same thing. But graphs in mathematics are spoken of as connected, not interconnected. Again, subtle usage but bad subtle usage adds up, damn it.
> sweeping dictionary between algebra and geometry that allowed mathematicians to do geometry over arbitrary rings, with arithmetic and infinitesimal data built in from the start.
That made me laugh, I wasn't expecting grothendieckian geometry to be described in LLM speak. What a time to be alive.
After they announced the formalization of the classification of Finite Simple Groups, I immediately wondered "What would happen if you tried to formalize the Stacks Project?" Despite also being very long, it's the opposite of the CFSG: instead of a poorly organized set of results that contribute to proving one big theorem, it's instead a carefully-organized set of results that cover a broad area.
The Stacks Project was the model for how mathematics should be done (at least for the pre-LLM era). Algebraic geometry had lots of poorly organized foundational results that were not really created for themselves, but in order to solve problems in the field. One person, Aise Johan de Jong, set out to fix it by organizing a project to write out the proofs of all of the results in a carefully organized fashion. He's led the project since, though of course there are multiple contributors. The whole thing is thousands of pages.
I would be interested in hearing more about the gaps they uncovered in the existing results, and how they fixed them.
I actually believe that this isn't the way to go when proof is cheap. Due to the straitjackets of type theory sharing proofs across domains is painful for most human readers to consume. With AI it's much easier to specialize theories. It's just not worth the cognitive cost to build on top of broad and shallow theories. To have any hope in keeping up with AI we need to instead better appeal to the largest component of our brain - namely our visual cortex.
The visual cortex is not the largest component of our brain.
Uh by "specialized theories" you mean less general results. Such a straightjacket is totally against the spirit of math.
Have you looked at how much Lean proofs are just translations between types?
Okay this is actually useful AI formalization. But the stacks project is basically Lean in natural language anyways, so it makes sense why its high quality.
Kind of ironic that (as of today) the most recent blog post from Oct 21 '26 on the original Stacks Project is "21 Oct 2026: No AI for now"
A very good friend of mine is an algebraic geometer and all of the AI progress in math is, to put it mildly, bumming him out. And me too honestly!
I understand the allure of doing this kind of work in AI on some level, but I'm becoming increasingly skeptical of generating "knowledge" that's difficult or impossible for humans to understand (at scale or otherwise).
The one bottleneck in this new AI era of math is still human understanding. No matter how much new stuff you can prove, to understand something you still have to basically do stuff the old fashioned way. Maybe AI can help a little, but without working through problems and proofs, you still won't get much farther. Ultimately our minds are limited that way.
I tend to think that the progress of mathematics before AI was roughly suited to the way humans assimilated understanding, but now with AI, the progress in mathematics is going to go much faster, oustripping our ability to understand it.
It is true that more mathematicians could theoretically eventually go through it, but the process of progress itself is discouraging and thus paradoxically renders this new AI era of math much less interesting to many.
I guarantee that after the intial "look at all the stuff we can prove", the benefits of using AI will dwindle rapidly.
Why would mathematicians want to build upon a corporate product? It's against the principles of free and open academic research.
Related:
https://news.ycombinator.com/item?id=40025362
Do they say how they verified the formalizations of the theorem hypotheses? (Sorry, I haven't read it yet.)
The fact that the description is AI slop doesn't inspire confidence in the results.
Slop Verbiage, Straight To Your HN Feed
Yes, "This milestone begins with the Stacks Project itself". Could half AI slop effects be mitigated by a prompt "Don't mix or mangle metaphors here"? A milestone is a step in a process, not the entire process.
Once this kind of sloppy effort to sound impressive was just "over writing" but its now a strong tell for AI.
Why is that a mixed metaphor? I'm very used to large initiatives/programs with several large milestones, each involving multiple projects. I don't see any issue with it.
The milestone they are reaching is the formalization of The Stacks Project. It began whenever they started prompting an AI to do that or started preplanning.
The metaphor of milestone is a goal reached within a larger process. I think that, yeah many people will not find a problem instances of this sort of (mis imo) usage but AIs to create a sequence of these things and that tends to create a tone to AI writing that many people can feel even if they can't point to particular problem usage.
Axiom raises $264M, publishes this massive lean proof built with AI, and you're moaning about some AI language in their description. AI is in their domain name. What are you doing?
Using AI isn't an excuse to use it badly. I mean, it's the constant excuse but shouldn't be.
what's bad about it? formless assertion has no content
I mentioned one AIism here: https://news.ycombinator.com/item?id=50383112
And here's another example of mangled word use: "creating a sweeping dictionary between algebra and geometry that allowed mathematicians to do geometry over arbitrary rings, with arithmetic and infinitesimal data built in from the start."
What does "sweeping dictionary" mean?! And I don't think "creating ... across" is the right to way to construct indirect objects. In old writing day I think it would be called an "awkward construction" but I everyone's very used to such awkward constructions AI tells.
Consider they/it could have said "creating a link between algebra and geometry that allowed mathematicians to do geometry over arbitrary rings, with arithmetic and infinitesimal data built in from the start. ", in fact that's the language I'm used to.
It's shame because twisting metaphors in an ad-hoc way can be a nice thing but LLMs do this constantly and badly and mother looks at the (simulated) kids and says "this is why we can't have nice things".
Edit: I can't help myself "...In a tightly interconnected dependency graph of definitions and theorems..."
Sure, connected and interconnected mean nearly the same thing. But graphs in mathematics are spoken of as connected, not interconnected. Again, subtle usage but bad subtle usage adds up, damn it.
“… built in from the start” is also hackneyed, and doesn’t fit the dictionary metaphor.
> sweeping dictionary between algebra and geometry that allowed mathematicians to do geometry over arbitrary rings, with arithmetic and infinitesimal data built in from the start.
That made me laugh, I wasn't expecting grothendieckian geometry to be described in LLM speak. What a time to be alive.
> What a time to be alive.
That's way more infuriating than hackneyed AI copy.
With that much money you'd think they could hire someone who took a writing class.
Slightly off-topic, but how far are we from a formally verified stack for (say) a webdav or NFS server?
The Stacks project concerns algebraic (and geometric) stacks - schemes generalised through descent (via sheaves, groupoid fibres etc)