Abstract: Mathematical proofs are traditionally verified by human experts, leaving room for undetected errors. Lean 4 is a proof assistant that mechanically checks each logical step, enabling reliable formal verification. This talk provides a brief introduction to Lean 4 and Mathlib, the largest library of formally verified mathematics, highlighting its role in advancing rigorous computational reasoning and its growing relevance at the intersection of programming and mathematics.
If you are interested in formalization and autoformalzation please contact yqing@utk.edu and check out opportunities at THRIVE 2026-2027: formalization and autoformalization.
Spring 2026
Feb 9 Conrad Plaut Singular Homology at Scale
Feb 23 Caglar Uyanik Singularity of Cannon-Thurston maps
March 2 Yulan Qing The Non-peripheral Curve Graphs
March 16 Pratit Goswani Dehn Functions of Coabelian Subgroups
April 13 Kavindya Jayathilaka Introduction to LEAN
April 20 Sagnik Jana
April 27 Inyoung Ryu
May 4 Ernesto J. Ugona S.
Fall 2025
September 8 Dominic Bair First Passage Percolation on Hyperbolic Graphs: Bi-infinite Geodesics, Radial Maps, and Infinitely Many Thick Triangles
September 22 Alex Squires One-endedness in Curve graphs
October 13 Sunrose Shrestha Cylinders on the Mucube
October 20 Ivy Dey Homotopy and Homology of Metric Spaces at Scale: A Framework for Quantitative Topology
October 27 Vicky Wen Sublinearly Morseness in Higher Rank Symmetric spaces
November 10 Roberta Shapiro Geometry, topology, and combinatorics of fine curve graphs
November 17 George Shaji Svarc-Milnor actions and asymptotic dimension for big mapping class groups.
Spring 2025
Feb 10 Spendcer Dowdall Geometric finiteness in mapping class groups: examples and perspectives
March 3 Xiangdong Xie Rigidity of pattern-preserving quasiisometries of nilpotent Lie groups
March 24 Koichi Oyakawa Geometry and dynamics of the extension graph of graph product of groups
April 21 Manisha Garg Units and zero-divisors of group rings over CAT(0) groups
April 28 Behrang Forghani Poisson boundary Identification Problem
Fall 2024
August 23, Friday Sagnik Jana Sublinearly Morse boundary
September 9 Rachel Skipper Braiding groups of homeomorphisms of the Cantor set
October 21 Meenakshy Jyothis Towards Ivanov’s meta-conjecture for geodesic currents
November 4 Alex Margolis Coarse homological invariants of metric spaces
November 11 Petr Kosenko Random walks on Fuchsian groups and Hardy spaces: an unexpected connection
November 25 Ekaterina Rybak Frattini subgroups of hyperbolic-like groups
December 2 Dimitrios Nikolakopoulos Log-Concavity of Characteristic Polynomial Coefficients in Representable Matroids
Spring 2024
Feb 26 Thomas Ng Quotients of free products
March 4 Mark Pengitore Residual finiteness growth functions of surface groups with respect to characteristic quotients
March 18 Sahana Balasubramanya The semi simple theory of acylindricity in higher rank
