Talks

Recent advances in automated theorem proving have made Lean 4 increasingly relevant to working mathematicians. Lean serves both as a proof assistant for human formalization and as a verification environment for automated systems. Its relevance to research-level mathematics was demonstrated by the Liquid Tensor Experiment, proposed by Peter Scholze and completed in 2022. More recent AI-assisted examples include the recent submission of P. Monticone’s Kourovka Notebook Problem 21.24, 20.125 and 20.150 solution notes from March 2026, which report that the solutions were autonomously discovered and formally verified in Lean 4 by Aristotle, a formal reasoning agent developed by Harmonic. In this talk, I will introduce mathlib, the largest library of formalized mathematics written in Lean, give a short proof demo, and discuss my recent progress formalizing finitely presented groups.

Recent advances in AI-assisted theorem proving have made Lean 4 increasingly relevant to working mathematicians. Lean serves both as a proof assistant for human formalization and as a verification environment for automated systems. Its relevance to research-level mathematics was demonstrated by the Liquid Tensor Experiment, proposed by Peter Scholze and completed in 2022. More recent AI-assisted examples include the recent submission of P. Monticone’s Kourovka Notebook Problem 21.24, 20.125 and 20.150 solution notes from March 2026, which report that the solutions were autonomously discovered and formally verified in Lean 4 by Aristotle, a formal reasoning agent developed by Harmonic. In this seminar, I will introduce the basic ideas of formalizing mathematics in Lean, give a short demo, and discuss my recent progress formalizing finitely presented groups for mathlib4, the largest library of formalized mathematics written in Lean.

A general-audience talk about a possible version of the future for mathematical discovery.

An account of my experience formalizing finitely presented groups as a beginner, told as a story for fellow beginners heading to the conference. I share what it was like to start out recently, with all these AI tools at our disposal.

This thesis explores how concepts of formal language theory can be used to study left-orderable groups. It analyses the languages formed by their positive cones and demonstrates how the abstract families of languages (AFLs) in the Chomsky hierarchy (in particular regular and context-free languages) interact with core group-theoretic constructions under subgroups, extensions, finite generation and taking direct products with $\mathbb{Z}$. These investigations yield new insights into the interplay between decidability and geometry in group theory. Some results which may be improvements to the existing literature are included in the thesis. There is a classification of the complexity of positive cones of $\mathbb{Z}^2$, a more constructive proof on finding regular positive cone languages of language-convex subgroups compared to a result of Su (2020), a construction of countably infinite many regular positive cones of $BS(1,q)$ for $q \geq -1$ which are all automorphic to each other extending a result of Antolín, Rivas, and Su (2022), and a construction of positive cones with finite generating set for groups of the form $F_{2n} \times \mathbb{Z}$ extending a result of Malicet, Mann, Rivas, and Triestino (2019).

An overview of my doctoral research on left-orderable groups and the formal-language complexity of their positive cones, aimed at a general mathematical audience with an emphasis on research motivations rather than technical detail.

A regular left-order on finitely generated group $G$ is a total, left-multiplication invariant order on $G$ whose corresponding positive cone is the image of a regular language over the generating set of the group under the evaluation map. We show that admitting regular left-orders is stable under extensions and wreath products and give a classification of the groups whose left-orders are all regular left-orders. In addition, we prove that solvable Baumslag-Solitar groups $B(1,n)$ admits a regular left-order if and only if $n\geq -1$. Finally, Hermiller and Sunic showed that no free product admits a regular left-order, however we show that if $A$ and $B$ are groups with regular left-orders, then $(A*B) \times \mathbb{Z}$ admits a regular left-order.

An introductory talk on left-orderable groups and the study of the formal-language complexity of their positive cones.

We propose a criterion for the regularity of a formal language representation when passing to subgroups. We use this criterion to show that the regularity of a positive cone language in a left-orderable group passes to its finite index subgroups, and to show that there exists no left order on a finitely generated acylindrically hyperbolic group such that the corresponding positive cone is represented by a quasi-geodesic regular language. We also answer one of Navas’ question by giving an example of an infinite family of groups which admit a positive cone that is generated by exactly $k$ generators, for every $k \geq 3$. As a special case of our construction, we obtain a finitely generated positive cone for $F_2 \times \mathbb{Z}$.