Kolloquium Wilhelm Killing

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.

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