@tao@mathstodon.xyz Thank you and all involved for putting this together! I have many thoughts on AI in math (as I'm sure we all do, especially given recent events). I think a decent analogy for the effects of indiscriminant use of AI to answer open questions unchecked (by humans) and without our proper understanding, is the use of AI to generate large portions of code in some codebase. Anyone who's used LLM for coding knows how quickly AI generated code can get beyond our understanding, due to the volume and all the definitions and sometimes obtuse ways of doing things. It seems like this is one of the issues which need to be addressed in the use of AI in math — yet-to-be checked (by humans) and understood (by humans) proofs are similar to unverified mass LLM generated code. And the difference in math vs. coding is the essential goal of math is in exactly that understanding, not in if the code compiles and program works (of course, not to say understanding code isn't important too in any professional program). But on one hand, is it right to fully cease AI's pursuit of solutions to problems? I think even if it proves something which is at the moment poorly understood, the output it gives _does_ give a route along which one can follow to themselves understand the new methods and discoveries the AI made to solve the problem, right? What if, we decide to create some new category of results: "Proven by AI" vs. "Verified by humans" ? And perhaps this second category could also ensure the methods used are properly attributed, of course (though this part may not be all that straightforward). I am curious what your thought are about that suggestion.