The Stacks Project, Formalized in Lean

Posted by namanbnsl 1 day ago

Comments

Comment by QuesnayJr 23 hours ago

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.

Comment by fspeech 15 hours ago

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.

Comment by eru 11 hours ago

The visual cortex is not the largest component of our brain.

Comment by Ericson2314 11 hours ago

Uh by "specialized theories" you mean less general results. Such a straightjacket is totally against the spirit of math.

Comment by fspeech 8 hours ago

Have you looked at how much Lean proofs are just translations between types?

Comment by jptlnk 17 hours ago

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).

Comment by bemtevi 16 hours ago

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.

Comment by vatsachak 23 hours ago

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.

Comment by throw567643u8 13 hours ago

Why would mathematicians want to build upon a corporate product? It's against the principles of free and open academic research.

Comment by nhatcher 15 hours ago

https://news.ycombinator.com/item?id=40025362

Comment by AlexCoventry 22 hours ago

Do they say how they verified the formalizations of the theorem hypotheses? (Sorry, I haven't read it yet.)

Comment by breezybottom 23 hours ago

The fact that the description is AI slop doesn't inspire confidence in the results.

Comment by viccis 23 hours ago

Slop Verbiage, Straight To Your HN Feed

Comment by browningstreet 22 hours ago

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?

Comment by breezybottom 16 hours ago

With that much money you'd think they could hire someone who took a writing class.

Comment by joe_the_user 21 hours ago

Using AI isn't an excuse to use it badly. I mean, it's the constant excuse but shouldn't be.

Comment by nh23423fefe 20 hours ago

what's bad about it? formless assertion has no content

Comment by joe_the_user 18 hours ago

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.

Comment by twoodfin 6 hours ago

“… built in from the start” is also hackneyed, and doesn’t fit the dictionary metaphor.

Comment by a57721 16 hours ago

> 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.

Comment by browningstreet 58 minutes ago

> What a time to be alive.

That's way more infuriating than hackneyed AI copy.

Comment by joe_the_user 22 hours ago

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.

Comment by falcor84 20 hours ago

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.

Comment by joe_the_user 18 hours ago

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.

Comment by eternauta3k 1 day ago

Slightly off-topic, but how far are we from a formally verified stack for (say) a webdav or NFS server?

Comment by lambdas 18 hours ago

The Stacks project concerns algebraic (and geometric) stacks - schemes generalised through descent (via sheaves, groupoid fibres etc)