Skip to content

Work

Publications

Mathematics

Finitely generated positive cones in $F_n \times \mathbb{Z}$

Abstract

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 toolbox for left-orders of low complexity (PhD thesis)

Regular left-orders on groups

joint with Yago Antolín and Cristóbal Rivas

Abstract

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.

Formal language convexity in left-orderable groups

Abstract

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

Formalization & AI

A dataset of formalised theorem statements from the Annals of Mathematics

Thomas Browning*, Katerina Hristova*, David Ledvinka*, Justus Springer*, Hang Lu Su, Jack McKoen and Kevin Buzzard† (*first authors; †principal investigator)

Abstract

Recent progress in autoformalisation of mathematics using AI has been impressive. Measuring this progress requires datasets of formal statements that are both hard and trustworthy. We present AnnalsChallenge: 50 formalised theorem statements written by hand in Lean 4 using mathlib. Each is the main result of a paper published in the Annals of Mathematics since 2020. Every formalisation was manually reviewed and then audited by AI. We release them without formalised proofs.

Formalization, Software & AI

Contributions to mathlib — December 2025–present

Definitions I added to mathlib, Lean’s largest mathematics library (merged pull requests):

Claude skills — Summer 2026

Skills I built for formalization work:

Contributions to other Lean projects

Computational group theory

Assorted programming projects

Recurse Center — Summer 2017

See more
  • Minimal chat server: a Python TCP chat server using threads and non-blocking sockets.
  • Sum of odd numbers animation: a p5.js visual proof that $1+3+\cdots+(2n-1)=n^2$, with Sukanya Aneja.
  • Magic tmux box: a Bash launcher that checks for an existing tmux session before starting one.
  • OK Bot: a Python Twitter bot that posts reassurance with links to matching tweets.

Expository writing

Expository papers

Introduction to $\ell^2$-Betti numbers — Spring 2016

Description

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.

Overview of the classification of tripartite entanglement under SLOCC — Summer 2014, warning: extreme juvenilia!

Description

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

Research notes

These are my research notes from old projects which did not turn into other material, in case it is of use to someone starting out a similar project. Warning: by the nature of these documents, some statements or ideas in there may be completely wrong.

Growth in the Heisenberg Group — Fall 2016

Keywords

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.

Last updated: 2026-10-17

Work - Hang Lu Su