The Stacks Project, Formalized in Lean
axiommath.ai
axiommath.ai
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.
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).
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.
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.
That made me laugh, I wasn't expecting grothendieckian geometry to be described in LLM speak. What a time to be alive.
That's way more infuriating than hackneyed AI copy.
Once this kind of sloppy effort to sound impressive was just "over writing" but its now a strong tell for AI.
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.