Past talks
Past talks in reverse chronological order. Click to unfold the abstract.
-
—— NO SEMINAR —
-
Kristian Latvanen (Aalto University)Formalizing percolation
Abstract
I will describe our current project on formalizing percolation theory, more specifically, sharpness of percolation phase transition. Due to advances in AI, the emphasis of the project has shifted somewhat, most recently due to a full LLM-generated formalization of the original goal by Anthropic. Especially, I will describe what has been learned in writing a Mathlib-quality version of the result and the usefulness of LLMs in it.
-
Thanh-Long Tran (University of Helsinki)Lean-augmented LLM infrastructure for research
Abstract
I will describe a multi-agent infrastructure I engineered for mathematical research, combining human-directed autonomous derivation with Lean-based verification and adversarial numerical tests. I will discuss how I directed this system to derive essentially the entirety of the mathematical results in one of my current research projects, while validating the derivation myself.
-
Niklas Halonen (University of Helsinki)Automated Grading in Lean Using Comparator
Abstract
In my talk, I give an introduction to Comparator and briefly explain the principles and challenges behind it. I will also demonstrate my tool for automated grading of Lean exercises called "comparator-autograder".
-
Janne Junnila (University of Jyväskylä)In search for practical autoformalization workflows for working mathematicians
Abstract
I will present a personal account of my own autoformalization experiments in complex analysis and related areas. This will include a demo of Handwave, which is a tool intended to help in planning, building, organizing and presenting autoformalized Lean projects.
-
Talal Alrawajfeh (University of Helsinki)Title to be announced