Seminar on Formalized Mathematics
The seminar meets Fridays at 13:15–14:00 in room U4062 of the main building of University of Helsinki (Fabianinkatu 33).
Anyone interested in formalization of mathematics is welcome!
Upcoming talks
-
Thanh-Long Tran (University of Helsinki)Lean-augmented LLM infrastructure for research
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.
-
Kristian Latvanen (Aalto University)Formalizing percolation
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.
-
—— NO SEMINAR —
Past talks
Past talks are listed in the archive.