Testbrett

Generative AI is rapidly transforming the landscape of mathematical research by solving many open mathematical problems. I will talk about these advances from the perspective of formalized mathematics. Many of these AI solutions come with an AI-generated formalization in Lean. These might not help to understand the mathematical argument, but do provide some guarantees about the correctness of the proof. I will discuss to what extent we can trust Lean formalizations and what there is left to check and my perspectives on autoformalization.

The polaron describes the interaction of a charged particle with a bosonic field. For a class of polaron-type models with regular particle-field interaction, I present a framework that allows us to compare ground state properties of the polaron to those of an explicitly diagonalizable Hamiltonian. For this, we will compare point processes associated with the two Hamiltonians in the sense of stochastic order. This can be applied in order to derive the strong-coupling asymptotics of the vacuum overlap and the expected boson number of the ground state at total momentum zero, as well as to show linear divergence of the effective mass in the coupling parameter.

Turning powerful language models into reliable scientific collaborators takes more than model quality: it demands rigorous verification, mathematical guardrails, and an architecture that lets coding agents run long-horizon experiments autonomously. In this talk, I will present a practical framework for AI-assisted research that aims to compress the research cycle. The framework turns general-purpose coding agents into autonomous research assistants through a five-level taxonomy of human-AI collaboration, a set of methodological commandments encoding scientific rigor, and a sandboxed environment supporting sessions from quick explorations to multi-day, multi-node experiments. I will discuss the possibilities and limitations of agentic AI in research, and briefly illustrate the framework.

tba

tba

tba

tba

tba