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) … Continue reading What even is mathematical output?