I am back with a few thoughts. I stopped reading all the trauma logs of mathematicians who recently got impacted by AI. Instead I switched to building a corpus of knowledge for why and how AI is interacting with mathematics. I teach this term a new course here at Adam Mickiewicz University. It's title is "Computer assisted solutions to mathematical problems". I proposed it because I realized in the last 6 months something important. A. It makes no sense to grieve the "good old ways". We should study to the bone how mathematics and computers interact. There are three levels: numeric, symbolic and formal. B. The only way to prepare yourself for the rise of the technology is to understand it well. You cannot understand the progress of AI in mathematics if you don't know how the models are trained on the symbolic representation of mathematical proofs, how the training goes, why specific transformer architectures, reinforcement learning and basically a huge amount of incredible insights gives in practice some new value in mathematics. C. It is incredibly fun to train your own models (yes I use generative models to help me build training pipelines too, otherwise I would not have enough lifetimes to do so). D. The AIxMaths space is so incredibly complex - you have these weird, scalable token generating algorithms, recently in agentic form with memory, interactions etc. This is a field of study - we need to understand how it works. On the other hand, mathematics as a field of science is incredibly complex, people do very different kinds of axiomatic theories with their intuitions, tactics and strategies. This was never studied too seriously as a whole. We need to study it deeply. So I am spending this term gearing up my students and myself for whatever is coming. We don't have any assumptions. I don't claim that models will become better at maths than all of human mathematicians. I don't think it's a good question. We just want to stay in the loop with the developments and see whether we can contribute to the change and see if this can be useful and productive. I am looking forward to your feedback. The current plan contains the following topics: - basic distinction between numerical computation, symbolic calculations and formal proofs - basic understanding of the IEEE 754 standard and things around numerical computations - how to build your own computer algebra system in Python and why it's so tricky - why and how proof-checking software is important; we start with the basic principles of such designes, I plan to talk first about the foundations going back to Automath and the foundational work of de Bruijn. - practical examples spanning real use cases of computer algebra, numerical integration and proofs in Peano arithmetic and how to read languages like Lean - in the end I want to present some little post-trained models like Qwen which I taught how to do Peano arithmetic better and how they prove statements about this theory; there will be AlphaGeometry too and maybe a bit more about Mizar, Metamath and Lean. Just to give students some scope and perspective. I plan to continue working on this course into a full book. I think I won't stop until I understand deeply why language models are currently so good at maths. It's something of utmost importance. It's important to see where this might stop and what lies beyond. I personally think these kind of questions will be the most important problems to answer by mathematicians themselves. We shouldn't stop until we find good answers to all of this. Reading AI slop is perhaphs a bit useful, but deep understanding of why it sometimes makes sense is even more challenging.