Work

We construct, for every even $n \ge 2$, a positive cone on $F_n \times \mathbb{Z}$ that is finitely generated as a semigroup, extending the previously known construction for $n = 2$. Malicet, Mann, Rivas and Triestino proved that $F_n \times \mathbb{Z}$ admits an isolated left-order if and only if $n$ is even. Since every finitely generated positive cone determines an isolated left-order, for $n \ge 2$, the group $F_n \times \mathbb{Z}$ admits a finitely generated positive cone if and only if $n$ is even.

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.

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}$.

Group Presentations API in mathlib4: the definition of Group.Presentation and starter API. Like Group.Generators, this is foundational geometric group theory needed by the AnnalsChallenge formalizations.

PRs:

• PR #41936 [Merged by Bors] - feat(GroupTheory/Presentation): define group presentations — Hang Lu Su

Group Generators API in mathlib4: the definition of Group.Generators and some auxiliary lemmas. This was part of my work for the AnnalsChallenge project.

PRs:

• PR #42437 [Merged by Bors] - feat(GroupTheory/Generators): define a group generators as a structure — Hang Lu Su

Lead contributor to the Finitely Presented Groups API. I first proposed this project at ItaLean2025 and it grew into a concrete mathlib project under the guidance of Riccardo Brasca, Kevin Buzzard and Thomas Browning. After I merged the definition of finitely presented groups into mathlib, participants of the Lean meetup I organize (MadLean) were given statements from the planned API to prove and submit themselves. Everyone involved was a first-time mathlib contributor! Along the way I mentored 5 new contributors through their first pull requests.

PRs:

• PR #34580 [Merged by Bors] - feat(Algebra/Group/Subgroup/Ker): kernel of a homomorphism composed with an isomorphism — Hang Lu Su
• PR #34621 [Merged by Bors] - feat(GroupTheory/FreeGroup/Basic): deprecate FreeGroup Empty ≃ Unit using Equiv.ofUnique, add Mul suggestion using MulEquiv.ofUnique and add FreeGroup α ≃* Multiplicative ℤ — Hang Lu Su
• PR #34624 [Merged by Bors] - feat(GroupTheory/FreeGroup/Basic): surjection between types induces surjection between free groups on those types — Hang Lu Su
• PR #35029 [Merged by Bors] - feat: the normal closure of an empty set is the trivial subgroup — Hang Lu Su
• PR #35033 [Merged by Bors] - feat: a group is finitely generated if and only if there exists a surjective homomorphism from a FreeGroup on an arbitrary finite type α to the group — Hang Lu Su
• PR #36858 [Merged by Bors] - feat(GroupTheory/FreeGroup/Basic): injection/bijection between types induces injection/bijection between free groups — Jorge Luis Mayoral Peréz
• PR #36873 [Merged by Bors] - feat(FinitelyPresentedGroup): Add Multiplicative ℤ instance — Hang Lu Su
• PR #36996 [Merged by Bors] - feat(GroupTheory/FinitelyPresentedGroup): add finitely presented groups, minimal API version — Hang Lu Su
• PR #38109 [Merged by Bors] - feat: add finitely presented instance for free groups — Pablo Castellanos
• PR #38114 [Merged by Bors] - feat(FinitelyPresentedGroup): add finite groups instance — Javier Gómez Gonzalez
• PR #38311 [Merged by Bors] - feat(FinitelyPresentedGroup): Additivize everything and add ℤ instance — Hang Lu Su
• PR #38866 [Merged by Bors] - feat(PresentedGroup): free-product of presentations is isomorphic to the presentation of the union (over the disjoint union of generators) — Jorge Luis Mayoral Peréz
• PR #38971 [Merged by Bors] - chore(FinitelyPresentedGroup): Use dot notation by default whenever possible and typo fix — Hang Lu Su
• PR #40200 feat(FinitelyPresentedGroup): add definitional equivalence with generating set given by S : Set G — Alessio Ferrarini
• PR #40332 [Merged by Bors] - feat(FinitelyPresentedGroup): free product of finitely presented is finitely presented — Jorge Luis Mayoral Peréz
• PR #40726 [Merged by Bors] - feat(FinitelyPresentedGroup): comap of finitely generated normal subgroup — Javier Gómez Gonzalez
• PR #40845 [Merged by Bors] - feat(FinitelyPresentedGroup): quotient of a finitely group by a subgroup which is finitely generated under normal closure is finitely presented — Miguel Laredo

GAP simulations used to conjecture and prove infinite families of positive cones of every rank $k \geq 3$, fully answering the Main Problem of A remarkable family of left orderable groups: central extensions of Hecke groups by A. Navas (2011), and to exhibit finitely generated positive cones for $F_{2n} \times \mathbb{Z}$, extending Ping-pong configurations and circular orders on free groups by Malicet, Mann, Rivas and Triestino (2019).

This algorithms generate the sphere counts for the three-dimensional Heisenberg group over the integers (nilpotent of step 2), and gives the sphere count in terms of its Malcev coordinates.

Algorithm for the division-ring completion of $\mathbb{Q}[F_2]$ via finite recursive data — the computation behind the Computation in the Completion of the Free Group Algebra talk (see the Talks page).

Assorted projects built during a batch at the Recurse Center.

The goal of this presentation is to set up the framework for $\ell^2$ - Betti Numbers from the point of view of von Neumann Algebras.

The goal of this document is to give the undergraduate reader an overview of tripartite quantum entanglement under SLOCC, with no background assumed.

Keywords: growth in groups, nilpotent groups, Malcev normal form, Carnot groups, Gromov, growth in the polynomial range, rational growth, Duchin, Shapiro, geodesics, Cayley graph, CC metric, complexity, polynomial-time algorithm.