I have a feeling that within a year or so, the venerable agda-unimath library will sadly become filled with slop and slop-derived code. What a shame!
I'm hoping that we can get Pterodactyl to the point, within the next two years, that it can support a new iteration of UniMath. I should at some point write something about my suggested guidance on the use of AI in formalisation, but it will be based on the following two principles:
1. We should place no normative constraints whatsoever on what resources people use to facilitate their own thinking. That is a private matter.
2. We should not allow even one line of LLM-generated code into a mathematical library.
Regarding implementation, that's in principle a different story, but I am also opposed to the inclusion of AI-generated code in proof assistants. I do believe LLMs can help with finding bugs and doing code review, and I wouldn't stop anyone from doing that.
The thing is that proof assistants are very sophisticated things where one maintains a lot of subtle invariants. You might think that an LLM could do it better than you, but when it leaves you behind, it will get stuck eventually and you'll never be able to dig it out (since you didn't keep up with it).
When you write code, the main thing you produce is your own understanding; software is the exhaust. When working in the cutting edge, your understanding is more important than any software artefact that you could possibly produce. You cannot afford to get lost.
