Please for now do not have your AI leave comments or leave comments containing material written by AI or have your AI do pull requests or submit pull requests containing material written by AI.
At least for the near future, I intend to continue updating and fixing the Stacks project by hand. Comments that are about things you noticed while reading the Stacks project (and that you typed into the box yourself) are very welcome! Similarly, if you have found a fix of something or a small improvement and you typed in the latex code yourself, please do send it to the stacks project email address or make a pull request.
In other words: for the moment I am continuing my work in the same manner. I have been lucky to have had a lot of input from people directly typing into the comment boxes as well as emailing me things (thank you!) and I hope that people will continue to be a part of this project:)
Finally, I would like to observe that anything you find using AI, I can also find using AI (and maybe I already have)!
Are you okay with people “forking” the Stacks Project, and starting their own AI-assisted variant? I am certainly not suggesting to do that! But Kevin Buzzard, Kim Morrison, Adam Topaz, Jeremy Avigad, et al., do seem to worry we will see such projects. They put out a statement about AI-administered math repositories. By the way, have you read what Richard Borcherds has been saying about AI in the past week?
Well the stacks project license does permit creating derivative works. So legally there is nothing stopping anyone from doing so without and okay from Johan. Although I do think that doing so without prior communication with Johan on this will be a sign of poor social judgement.
@Jason can you give a pointer to where Borcherds was posting this?
Hi David, The articles I read were in the Daily Cal, the student paper of U C Berkeley (my alma mater): https://www.dailycal.org/news/campus/academics/uc-berkeley-math-community-left-at-crossroads-in-wake-of-openai-navier-stokes-proof/article_2253ca6c-39c0-45be-947a-f0fd5b48bd6c.html
To me, the idea of someone forking The Stacks Project would be as if after Deligne’s “Théorie de Hodge I” someone had said: ah, let me write my own follow-ups II and III. It may not betray the maths, but it betrays the vision of those who invested energy in starting something. I doubt any forked competitor to The Stacks Project would receive the same love, care and attention to detail without the aura of a community-driven project.
Let’s be real: a lot of young folks were (secretly) mega-proud when they found a gap in a proof and could fix it. A feeling of contribution, and sometimes, a feeling “of being be seen / being noticed”. I suspect that any forks would be very lonely places. Digital worlds without an ability to raise a happy little family of readers and contributors.
Axiom Math seems to have ignored your request. They have strip mined Stack project repository. See https://x.com/axiommathai/status/2118028838517219335 and this https://axiommath.ai/research/the-stacks-project-formalized/
Shame on you Axiom Math.
Isn’t Ken Ono at Axiom? What was he thinking?
Yes he is. Apparently this is actually his idea which makes it even more troubling. The whole purpose of this is marketing for Axiom Math as indicated by their social media posts and incessant self promotion of this “achievement”. What’s next? “Leanification” of every Springer Verlag yellow GTM textbook? Due to the brute automatic nature of this work, I am sure this is eminently possible to do, but why do it in this manner? Lean verification is really a guise to get training date for free …