OpenAI and Anthropic recently announced that their AI models disproved the Exponential Time Hypothesis (ETH), which (if confirmed) would be a major breakthrough in complexity theory. ETH states (roughly) that 3-SAT cannot be solved in subexponential time, i.e. time 2^o(n), so it is much stronger than the P ≠ NP statement. During the talk I will introduce ETH, its variant Strong ETH and their role in the area called Fine Grained Complexity. Next I will try to discuss what the fact that ETH is false means for this area. I will also briefly sketch the proof approach taken by OpenAI, based on the exposition given by Ryan O'Donnell.

In this talk I will show how the latest AI tools can be used in practice to do mathematics differently, while keeping a sense of meaning and purpose. I will introduce the notion of the agentic loop, auto-research, the role of skills, and the (auto)formalization of mathematical documentation at multiple levels. All of this will be illustrated with concrete projects in algebra, number theory, and beyond.

The talk is aimed in particular at mathematicians whose picture of AI comes from rather underwhelming chatbots. I will try to dispel that impression and show that the useful way to bring AI into mathematics goes through agents and through building specifications and computational architectures, and that this is far less complicated than it sounds.

I will give a one-hour introduction to the Lean 4 proof assistant, aimed at mathematicians. We will cover:
1) the main theoretic concepts of Dependent Type Theory and the Curry–Howard equivalence;
2) how it is realized in Lean 4 and what the main design choices are;
3) a number of small examples of "human-made" formalizations in Lean 4;
4) an overview of current capabilities of large reasoning models in writing Lean code;
5) a short discussion on the level of trust we can have towards Lean 4 proofs.

This summer mathematics changed faster than most of us could follow. This is a short status report: facts, not opinions.

Sometimes the role of AI is documented: a self-taught neurosurgery resident obtained a proof of Crouzeix's conjecture from a commercially available AI model. More often we can only reason statistically, as with tornadoes and global warming. I will show a burst of follow-ups on the Komlós conjecture, a group posting claimed solutions in unrelated fields every week, formal proofs in Lean, and a sharp change in arXiv combinatorics.

The rest of the meeting belongs to the discussion.