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.
eternauta3k 4 hours ago [-]
Slightly off-topic, but how far are we from a formally verified stack for (say) a webdav or NFS server?
vatsachak 3 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.
AlexCoventry 3 hours ago [-]
Do they say how they verified the formalizations of the theorem hypotheses? (Sorry, I haven't read it yet.)
breezybottom 4 hours ago [-]
The fact that the description is AI slop doesn't inspire confidence in the results.
viccis 4 hours ago [-]
Slop Verbiage, Straight To Your HN Feed
browningstreet 2 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?
joe_the_user 1 hours ago [-]
Using AI isn't an excuse to use it badly. I mean, it's the constant excuse but shouldn't be.
nh23423fefe 58 minutes ago [-]
what's bad about it? formless assertion has no content
joe_the_user 2 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.
falcor84 24 minutes 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.
Rendered at 21:20:55 GMT+0000 (Coordinated Universal Time) with Vercel.
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.
Once this kind of sloppy effort to sound impressive was just "over writing" but its now a strong tell for AI.