Kolloquium Wilhelm Killing

I will present an overview of the results on existence and asymptotic properties of magnetic skyrmions defined as topologically nontrivial maps of degree +1 from the plane to a sphere which minimize a micromagnetic energy containing the exchange, perpendicular magnetic anisotropy and interfacial Dzyaloshinskii-Moriya interaction (DMI) terms. In ultrathin films, the stray field energy simply renormalizes the anisotropy constant at leading order, but in finite samples it also produces additional non-trivial contributions at the sample edges, promoting nontrivial spin textures. Starting with the whole space problem, I will first discuss the existence of single skyrmions as global energy minimizers at sufficiently small DMI strength. Then, using the quantitative rigidity of the harmonic maps I will present the asymptotic characterization of single skyrmion profiles both in infinite and finite samples. Lastly, I will touch upon the question of existence of multi-skyrmion solutions as minimizers with higher topological degree and present recent existence results obtained jointly with T. Simon and V. Slastikov.

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