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.
- Preprint — August 2026 (submitted)
- Main results autoformalized in Lean 4: Palomar registry entry — October 2026
A toolbox for left-orders of low complexity (PhD thesis)
- ArXiv — December 2025
- Talk video; slides
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.
- Preprint — accepted in the Journal of Combinatorial Algebra, November 2022
- Talk video; slides — November 2020
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}$.
- Preprint — accepted in the International Journal of Algebra and Computation, May 2020
- Talk video; Slides — UPV, Bilbao, February 2020; Heriot-Watt, Edinburgh, March 2020
- Poster — YGGT, Bilbao, July 2019
- Lightning talk slides — Of Coarse!, Ventotene, September 2019
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.
- Preprint — October 2026
- Poster — NeurIPS 2026 Workshop MATH-AI, December 2026
- AnnalsChallenge repository
Formalization, Software & AI
Contributions to mathlib — December 2025–present
Definitions I added to mathlib, Lean’s largest mathematics library (merged pull requests):
- Finitely presented groups and finitely normally generated subgroups, as lead contributor. I proposed the project at ItaLean2025, and it grew under the guidance of Riccardo Brasca, Kevin Buzzard and Thomas Browning. While developing this API, I mentored five first-time mathlib contributors from MadLean.
- Group generators and group presentations.
- The word product, word length, word metric and geodesic words.
- The Gromov product, with Katerina Hristova.
- In review: hyperbolic metric spaces and hyperbolic groups with Katerina Hristova, and left-orderable groups, my PhD topic, with Yaël Dillies.
Claude skills — Summer 2026
Skills I built for formalization work:
- mathlib-api: A/B tests mathlib design decisions, using precedents already in the library as evidence.
- human-prose, adaptive-teacher and pair-programming: make Claude’s explanations easier to read and to learn from.
Contributions to other Lean projects
- Contributed statements of Kourovka Problem 8.8(b) and whether every hyperbolic group is residually finite to Google DeepMind’s formal-conjectures, plus supporting cohomology lemmas and notation to HodgeConjecture, using AI-assisted workflows.
Computational group theory
- Positive cones of every rank (2018 and 2025): GAP simulations that helped me conjecture, then prove, infinite families of positive cones of every rank $k \geq 3$. These families fully answer the main problem of Navas (2011). The simulations also exhibited finitely generated positive cones for $F_{2n} \times \mathbb{Z}$, extending Malicet, Mann, Rivas and Triestino (2019).
- Sphere counts in the Heisenberg group (2016–2017): SageMath code that computes sphere counts for the integer Heisenberg group in Malcev coordinates.
- Completion of the free group algebra (2015): an algorithm for the division-ring completion of $\mathbb{Q}[F_2]$ via finite recursive data (slides; talk on the Talks page).
Assorted programming projects
Recurse Center — Summer 2017
- A Metamath-to-SAT translator, a toy blockchain and a raytracer, all in Python.
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