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.
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.
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?
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.
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.
Slightly off-topic, but how far are we from a formally verified stack for (say) a webdav or NFS server?
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.
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
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
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.