For those interested in getting started with blueprint-driven formalisation projects in Lean, I created a template repository (from which the InfinityCosmos project was generated) with the tutorial I presented at the Hausdorff Center for Mathematics in Bonn.

📂 Repository: https://github.com/pitmonticone/LeanProject
🎥 Video: https://youtu.be/KyuyTsLgkMY

I am belatedly realizing that in my attempts to describe my evaluation of the capability of an AI tool, I inadvertently gave the incorrect (and potentially harmful) impression that human graduate students could be reductively classified according to a static, one dimensional level of “competence”. This was not my intent at all; and I would therefore like to make the following clarifying remarks.

Firstly, the ability to contribute to an existing research project is only one aspect of graduate study, and a relatively minor one at that. A student who is not especially effective in this regard, but excels in other dimensions such as creativity, independence, curiosity, exposition, intuition, professionalism, work ethic, organization, or social skills can in fact end up being a far more successful and impactful mathematician than one who is proficient at assigned technical tasks but has weaknesses in other areas.

Secondly, and perhaps more importantly, human students learn and grow during their studies, and areas in which they initially struggle with can become ones in which they are quite proficient at after a few years; and personally I find being able to assist students in such transitions to be one of the most rewarding aspects of my profession. In contrast, while modern AI tools have some ability to incorporate feedback into their responses, each individual model does not truly have the capability for long term growth, and so can be sensibly evaluated using static metrics of performance. However, I believe such a fixed mindset is not an appropriate framework for judging human students, and I apologize for conveying such an impression.