What even is mathematical output?

It’s been nearly a week since the dump of the GitHub repository with over 700 documents and (far fewer) Lean formalisations of AI-generated proofs, but it’s felt a lot longer. My own views on use of AI are mixed. I use it for my day job, we formalise things (previously in Isabelle, now in Lean) that we are implementing, and which will never be made public. I have played around with AI to fill in my understanding of background material for a research paper I’m writing, and to try to hunt for references for things that are difficult to find, and to generate some code that calculates something in a specialist language I didn’t know. I have used it to translate and extract material out of old scanned documents. But I am loath to just get it to prove things I want to know. A couple of years back I did, when the systems were much more flaky, and eventually I ended up just deriving what I got out of it by hand from scratch, as I lost the transcript and I needed a proof anyway. I choose not…