Daniel Halpern-Leistner

Algebraic Geometry, Derived Categories, Machine Learning for Math, Representation Theory

Associate Professor in Mathematics, Cornell University, CV link, email: daniel.hl@cornell.edu

monodromy

Recent Activity

  • New Paper: A categorical perspective on non-abelian localization. (Sept. 2025) Develops a new method to study the derived category of quasi-coherent sheaves on stacks with a $\Theta$-stratification, with applications to enumerative geometry.

    View Paper →

  • Research Project: Autoformalization for the working mathematician benchmark. An effort to develop a benchmarking dataset for autoformalization of mathematics, with special emphasis on tasks that are useful for research mathematicians, beginning in June, 2025.

    View Github Repo →

  • Conference Talk: On the alignment problem in mathematics at the Stevens Institute of Technology, June 2025. An invitation for mathematicians to play an active role in the development of AI tools. I announce a community project to construct a dataset for training autoformalization systems.

    View Slides →

  • Conference Talk: Moduli spaces of objects in dg-categories at the Homological Mirror Symmetry conference in honor of Maxim Kontsevich's 60th birthday, January 2025. I use recent results in moduli theory to give an intrinsic formulation of homological mirror symmetry, and I introduce some conjectures in symplectic topology that would imply it. I gave a similar talk at the 2025 Summer Research Institute in Algebraic Geometry, July 2025

    View Slides →

  • Upcoming: Invited speaker at the International Congress of Mathematicians, Summer 2026
Dan H-L

Research

Below is a selection of my research projects, organized into three main themes. A full and up-to-date list of my articles is available here and on my Google Scholar page.

Moduli Theory, Beyond GIT

My work built a bridge between geometric invariant theory, which is a collection of results describing the orbit structure for the action of a reductive group on an algebraic variety, with the intrinsic approach to moduli theory in algebraic geometry, i.e., the theory of algebraic stacks. In the past few years, I have been focused on applying the general theory to various moduli problems of interest in algebraic geometry.

Structure of Derived Categories

The derived category of a variety $X$ is an $\infty$-category that encodes all information about coherent sheaves on $X$ and their cohomology. Remarkably, derived categories often have structures and symmetries that are not visible on the level of coherent sheaves alone. My work has shed light on these structures, especially in the setting of equivariant coherent sheaves for the action of a group on $X$, taking inspiration from mathematical physics and homological mirror symmetry.

Machine Learning for Mathematics

Since 2017, I have had a side interest in machine learning, and it has recently taken a larger role in my research effort. I have investigated applications of reinforcement learning to computer algebra, and more recently applications of large language models to formalization of mathematical arguments.

Moduli Theory, Beyond GIT

Thumbnail
Towards a general theory of instability in moduli theory

A common kind of problem in algebraic geometry is to find a space, called a moduli space, parameterizing isomorphism classes of some kind of algebro-geometric objects -- let's call them widgets. Many attempts to form a moduli space for widgets proceed by finding a scheme, $X$, which parameterizes a family of widgets, and an algebraic group, $G$, acting on $X$ such that points in the same orbit under $G$ parameterize isomorphic widgets. Then hopefully one can apply geometric invariant theory to find an open subset in X which has a good quotient under the action of $G$, and whose $G$-orbits classify ``semistable'' widgets. However, there are many situations where a stability condition can be specified on widgets without referring to any GIT problem. We discuss a framework for defining a notion of semistability for an arbitrary moduli problem, and we introduce a structure on the unstable locus, which we call a Theta-stratification, which generalizes classical stratifications of the unstable locus in GIT as well as of the moduli of vector bundles on a curve. We identify a class of moduli problems, which we call $\Theta$-reductive, for which the GIT story carries over nicely into this more general framework -- for these stacks the existence of a $\Theta$-stratification on the unstable locus can be reduced to checking a relatively simple hypothesis.

  • "On the structure of instability in moduli theory," (arXiv)
  • Updated version here. (Last update 2/2/2022)
Thumbnail
Intrinsic Donaldson-Thomas theory. I. Component lattices of stacks

Joint with Chenjing Bu, Andrés Ibáñez Núñez, and Tasuki Kinjo. This is the first, more foundational, part of a series of papers by my coauthors (not me) attempting to generalize Joyce's wall-crossing formalism from the context of objects in abelian categories to much more general moduli stacks.

Abstract: This is the first paper in a series on intrinsic Donaldson-Thomas theory, where we develop a new framework for enumerative geometry that allows the generalization of constructions and results from linear moduli stacks to general non-linear algebraic stacks. In this paper, we introduce the component lattice of an algebraic stack. This is a key object in our theory, defined using the formalism of stacks of graded and filtered points. It provides the combinatorial data needed to formulate various results in enumerative geometry, such as decomposition-type theorems and wall-crossing formulae. Later papers in the series will focus on extending Donaldson-Thomas theory to the non-linear case, and we expect that our approach will be useful for extending many other flavours of enumerative invariants beyond the linear case as well. This paper proves several foundational results of our framework. The first is the constancy theorem, which states that the isomorphism types of connected components of the stacks of graded and filtered points stay constant within chambers in the component lattice. The second is the finiteness theorem, which provides a criterion for the finiteness of the number of possible isomorphism types of these components. The third is the associativity theorem, generalizing the structure of Hall algebras from linear stacks to general stacks. We also discuss some applications of these results outside Donaldson-Thomas theory, including a construction of stacks of real-weighted filtrations, and a generalization of the semistable reduction theorem to real-weighted filtrations.

View Paper →

Thumbnail
Projectivity of the moduli of equidimensional branchvarieties

Joint with Andres Fernandez Herrero, Trevor Jones, and Ritvik Ramkumar, I investigated alternative approaches to constructing moduli of polarized varieties using geometric invariant theory on moduli spaces of branchvarieties. These moduli spaces provide alternatives to Hilbert schemes.

Abstract: We resolve an open problem posed by Alexeev-Knutson on the projectivity of the moduli of branchvarieties in the equidimensional case. As an application, we construct projective moduli spaces of reduced equidimensional varieties equipped with ample linear series and subject to a semistability condition.

View Paper →

Thumbnail
The local structure of algebraic stacks

"Artin algebraization for pairs with applications to the local structure of stacks and Ferrand pushouts" with Jack Hall and David Rydh: We give a variant of Artin algebraization along closed subschemes and closed substacks. Our main application is the existence of étale, smooth, or syntomic neighborhoods of closed subschemes and closed substacks. In particular, we prove local structure theorems for stacks and their derived counterparts and the existence of henselizations along linearly fundamental closed substacks. These results establish the existence of Ferrand pushouts, which answers positively a question of Temkin-Tyomkin.

View Paper →

Thumbnail
Infinite dimensional GIT

Given a numerical invariant on an algebraic stack, the general theory of $\Theta$-stability provides criteria that imply that the numerical invariant defines a $\Theta$-stratification, and that the semistable locus admits a good moduli space. The first criterion is called "monotonicity", and the second is called "HN boundedness." In the projects below, joint with Andres Fernandez-Herror and Trevor Jones, I developed a method for verifying monotonicity that is an infinite-dimensional analog of geometric invariant theory, in that it applies (roughly speaking) to ind-algebraic groups acting on ind-projective ind-schemes. In the second project, we apply this method and develop a new method for verifying HN-boundedness for the stack of maps from a smooth curve to a quotient stack.

  • "Moduli spaces of sheaves via affine Grassmannians" with Andres Fernandez Herrero and Trevor Jones: We develop a new method for analyzing moduli problems related to the stack of pure coherent sheaves on a polarized family of projective schemes. It is an infinite-dimensional analogue of geometric invariant theory. We apply this to two familiar moduli problems: the stack of -modules and the stack of pairs. In both examples, we construct a -stratification of the stack, defined in terms of a polynomial numerical invariant, and we construct good moduli spaces for the open substacks of semistable points. One of the essential ingredients is the construction of higher dimensional analogues of the affine Grassmannian for the moduli problems considered.

    View Paper →

  • "The structure of the moduli of gauged maps from a smooth curve" with Andres Fernandez Herrero: For a reductive group $G$, Harder-Narasimhan theory gives a structure theorem for principal $G$ bundles on a smooth projective curve $C$. A bundle is either semistable, or it admits a canonical parabolic reduction whose associated Levi bundle is semistable. We extend this structure theorem by constructing a $\Theta$-stratification of the moduli stack of gauged maps from $C$ to a projective-over-affine $G$-variety $X$. The open stratum coincides with the previously studied moduli of Mundet semistable maps, and in special cases coincides with the moduli of stable quasi-maps. As an application of the stratification, we provide a formula for K-theoretic gauged Gromov-Witten invariants when $X$ is an arbitrary linear representation of $G$. This can be viewed as a generalization of the Verlinde formula for moduli spaces of decorated principal bundles. We establish our main technical results for smooth families of curves over an arbitrary Noetherian base. Our proof develops an infinite-dimensional analog of geometric invariant theory and applies the theory of optimization on degeneration fans.

    View Paper →

Thumbnail
Moduli of $K$-semistable Fano varieties

There is a notion of K-stability for Fano varieties, which arose in the study of canonical Kaehler metrics in differential geometry. The ``Donaldson-Tian-Yau'' conjecture predicted that a Fano manifold admits a constant scalar curvature Kaehler metric if and only if it is K-polystable, and it was recently proved by Chen-Donaldson-Sun. K-stability is very naturally an instance of $\Theta$-stability, and it turns out that the beyond GIT framework works very nicely for the stack of Fano varieties (with klt singularities), eventually giving a $\Theta$-stratification and good moduli space for the semistable locus. I collaborated on two pieces of this story:

  • "On properness of $K$-moduli spaces and optimal degenerations of Fano varieties" with Harold Blum, Yuchen Liu, and Chenyang Xu: We establish an algebraic approach to prove the properness of moduli spaces of K-polystable Fano varieties and reduce the problem to a conjecture on destabilizations of K-unstable Fano varieties. Specifically, we prove that if the stability threshold of every K-unstable Fano variety is computed by a divisorial valuation, then such K-moduli spaces are proper. The argument relies on studying certain optimal destabilizing test configurations and constructing a Theta-stratification on the moduli stack of Fano varieties.

    View Paper →

  • "Reductivity of the automorphism group of K-polystable Fano varieties" with Jarod Alper, Harold Blum, and Chenyang Xu: We prove that K-polystable log Fano pairs have reductive automorphism groups. In fact, we deduce this statement by establishing more general results concerning the S-completeness and $\Theta$-reductivity of the moduli of K-semistable log Fano pairs. Assuming the conjecture that K-semistability is an open condition, we prove that the Artin stack parametrizing K-semistable Fano varieties admits a separated good moduli space.

    View Paper →

Thumbnail
Mapping stacks and the notion of properness in algebraic geometry

One essential feature of a scheme $X$ which is flat and proper over a base $S$ is that for any scheme $Y$ which is of finite type over $S$, there is an algebraic space $Map(X,Y)$ classifying maps from $X$ to $Y$. There are extensions of this statement when $X$ is a proper stack over $S$ and $Y$ has some reasonable hypotheses. While studying the notion of instability in algebraic geometry, I noticed that the quotient stack $\bC / \bC^\ast$ has this property as well. This lead to long investigation with Anatoly Preygel into just what properties of a stack X guarantee the existence of algebraic mapping stacks into "geometric" target stacks. We reformulated the notion of "properness" for algebraic stacks in terms of properties of the derived category of those stacks, in such a way that these categorical properties guarantee the existence of algebraic mapping stacks. Our notion generalizes the classical definition of proper Artin stacks, but in addition there are many global quotient stacks which are definitely not proper in the classical sense but are "proper" in our sense. We were able to construct a very large class of examples by introducing a notion of "projective morphism" of stacks, a property which can be readily verified in examples. Along the way, we prove some surprising new descent properties for derived categories of coherent sheaves in derived algebraic geometry.

  • "Mapping stacks and categorical notions of properness," with Anatoly Preygel (arXiv:1402.3204)
Thumbnail
Cartan-Iwahori-Matsumoto decompositions for reductive groups

We provide a short and self-contained argument for the existence of Cartan-Iwahori-Matsumoto decompositions for reductive groups.

  • "Cartan-Iwahori-Matsumoto decompositions for reductive groups" with Jarod Alper and Jochen Heinloth (arXiv:1903.00128)
Thumbnail
Existence of moduli spaces for algebraic stacks

We provide necessary and sufficient conditions for when an algebraic stack admits a good moduli space. This theorem provides a generalization of the Keel-Mori theorem to moduli problems whose objects have positive dimensional automorphism groups. We also prove a semistable reduction theorem for points of algebraic stacks equipped with a $\Theta$-stratification. Using these results we find conditions for the good moduli space to be separated or proper. To illustrate our method, we apply these results to construct proper moduli spaces parameterizing semistable $G$-bundles on curves.

  • "Existence of good moduli spaces for algebraic stacks" with Jarod Alper and Jochen Heinloth (arXiv:1812.01128)
Thumbnail
Tannaka duality revisited

Any map between algebraic stacks $f: \fX \to \fY$ yields a symmetric monoidal functor between derived categories of quasicoherent sheaves $f^\ast : QC(\fY) \to QC(\fX)$. Jacob Lurie showed that when $\fY$ is geometric (meaning quasicompact with affine diagonal), $f$ can be uniquely recovered from $f^\ast$, and the symmetric monoidal functors arising in this way are those satisfying certain hypotheses (continuous, preserving connective objects and flat objects). We generalize this result, showing that for many stacks, it is not necessary to show that $f$ preserves flat objects. This seemingly minor modification allows for a much wider range of applications of this "Tannakian formalism."

"Tannaka duality revisited" with Bhargav Bhatt (arxiv:1507.01925)

Structure of Derived Categories

Thumbnail
A categorical perspective on non-abelian localization

This is a short note which discusses a construction involving equivariant derived categories which allows one to state a categorical version of the classical Atiyah-Bott localization formula. The classical theorem states that for a smooth manifold with a $\bC^\ast$-action, the fundamental class in equivariant cohomology can be decomposed as a finite sum with each term corresponding to a connected component of the fixed locus, but in order to do this one must formally invert certain elements in the equivariant cohomology of the point. We show that if $X$ is a smooth scheme, then the structure sheaf of $X$ admits a filtration whose associated graded pieces correspond to connected components of the fixed locus, but in order to do this one must work in a slightly larger category of equivariant complexes, which we define.

Original draft version: "A categorification of the Atiyah-Bott localization formula; last update 5/21/2016 Final version, on arXiv: A categorical perspective on non-abelian localization

Thumbnail
The boundary of the stability manifold
In several projects, I have studied a partial compactification of the space of Bridgeland stability conditions on a triangulated category, called the space of augmented stability conditions. It has lead to some insights -- the conjecture that this space is a manifold with corners for smooth and proper dg-categories implies very broad existence results for proper moduli spaces of semsitable objects in those categories.
  • "The space of augmented stability conditions" with Alekos Robotis: Given a triangulated category $\mathcal{C}$, we construct a partial compactification, de\-noted $Astab(\mathcal{C})$, of the quotient of its stability manifold by $\bC$. The purpose of $\Astab(\mathcal{C})$ is to shed light on the structure of semiorthogonal decompositions of $\mathcal{C}$. A point of $Astab(\mathcal{C})$, called an augmented stability condition on $\mathcal{C}$, consists of a newly introduced homological structure called a multi-scale decomposition, along with stability conditions on subquotient categories of $\mathcal{C}$ associated to this multi-scale decomposition. A generic multi-scale decomposition corresponds to a semiorthogonal decomposition along with a configuration of points in $\bC$. We give a conjectural description of open neighborhoods of certain boundary points, called the \emph{manifold-with-corners conjecture}, and we prove it in a special case. We show that this conjecture implies the existence of proper good moduli spaces of Bridgeland semistable objects in $\mathcal{C}$ when $\mathcal{C}$ is smooth and proper, and discuss some first examples where the manifold-with-corners conjecture holds.

    View Paper →

  • "Stability conditions and semiorthogonal decompositions I: quasi-convergence" with Jeffrey Jiang and Alekos Robotis: We develop a framework relating semiorthogonal de-compositions of a triangulated category $\mathcal{C}$ to paths in its space of stability conditions. We prove that when $\mathcal{C}$ is the homotopy category of a smooth and proper idempotent complete pre-triang\-ulated dg-category, every semiorthogonal decomposition whose fac\-tors admit a Bridgeland stability condition can be obtained from our framework.

    View Paper →

Thumbnail
The noncommutative minimal model program

This note aims to clarify the deep relationship between birational modifications of a variety and semiorthogonal decompositions of its derived category of coherent sheaves. The result is a conjecture on the existence and properties of canonical semiorthogonal decompositions, which is a noncommutative analog of the minimal model program. We identify a mechanism for constructing semiorthogonal decompositions using Bridgeland stability conditions, and we propose that through this mechanism the quantum differential equation of the variety controls the conjectured semiorthogonal decompositions. We establish several implications of the conjectures: one direction of Dubrovin's conjecture on the existence of full exceptional collections; the $D$-equivalence conjecture; the existence of new categorical birational invariants for varieties of positive genus; and the existence of minimal noncommutative resolutions of singular varieties. Finally, we verify the conjectures for smooth projective curves by establishing a previously conjectured description of the stability manifold of $\mathbb{P}^1$.

View Paper →

Thumbnail
Full exceptional collections on GIT quotients

Joint with Kimoi Kemboi.

We produce full strong exceptional collections consisting of vector bundles on the geometric invariant theory quotient of certain linear actions of a split reductive group $G$ of rank two. The vector bundles correspond to irreducible $G$-representations whose weights lie in an explicit bounded region in the weight space of $G$. We also describe a method for constructing more examples of linear GIT quotients with full strong exceptional collections of this kind as ``decorated" quiver varieties.

View Paper →

Thumbnail
Derived $\Theta$-stratifications and the D-equivalence conjecture

A follow up to "The derived category of a GIT quotient." The theory of $\Theta$-stratifications generalizes a classical stratification of the moduli of vector bundles on a smooth curve, the Harder-Narasimhan-Shatz stratification, to any moduli problem that can be represented by an algebraic stack. We use methods from derived algebraic geometry to develop a structure theory, which is a refinement of the theory of local cohomology, for the derived category of quasi-coherent complexes on an algebraic stack equipped with a $\Theta$-stratification. We then apply this to the $D$-equivalence conjecture, which predicts that birationally equivalent Calabi-Yau manifolds have equivalent derived categories of coherent sheaves. We prove that any two projective Calabi-Yau manifolds that are birationally equivalent to a smooth moduli space of Gieseker semistable coherent sheaves on a $K3$ surface have equivalent derived categories. This establishes the first known case of the $D$-equivalence conjecture for a birational equivalence class in dimension greater than three.

  • "Derived $\Theta$-stratifications and the D-equivalence conjecture." (draft; last update 10/01/20)
  • These results were originally announced in the paper ``Theta-stratifications, Theta-reductive stacks, and applications"

Preliminary versions: The above paper unites, generalizes, and corrects minor errors in two previous notes. I am preserving them here for reference.

  • "The D-equivalence conjecture for moduli spaces of sheaves on a K3 surface" (draft; last update 2/08/17) -- proves that under suitable genericity hypotheses, a variation of good moduli space for a derived stack with self-dual cotangent complex results in a derived equivalence, and sketches the main application to the D-equivalence conjecture.
  • "An appendix to 'Theta stratifications and derived categories'" (draft; last update 2/04/15) -- proves a version of the main theorem for global quotient stacks, which is enough for many applications
Thumbnail
The equivariant Verlinde formula on the moduli of Higgs bundles

The Verlinde formula expresses the dimension of the space of global sections of certain "determinant" line bundles on the moduli of principal $G$ bundles on a smooth curve $\Sigma$, where $G$ is a semisimple group. We prove an analog of the Verlinde formula on the moduli space of semistable meromorphic $G$-Higgs bundles over a smooth curve for a reductive group $G$ whose fundamental group is free. The formula expresses the graded dimension of the space of sections of a positive line bundle on the moduli space of Higgs bundles as a finite sum whose terms are indexed by formal solutions of a generalized Bethe ansatz equation on the maximal torus of $G$.

"The equivariant Verlinde formula on the moduli of Higgs bundles" with an appendix by Constantin Teleman (arxiv:1608.01754)

Thumbnail
Combinatorial constructions of derived equivalences

This proves a version of what I like to call the ``magic windows" theorem for a fairly general class of quotient stacks: those which are quotients of a linear representation $V$ of a reductive group $G$ (where the representation is ``quasi-symmetric"). The magic windows theorem identifies (under some mild hypotheses) a subcategory of the equivariant derived category of coherent sheaves on $V$ with the derived category of coherent sheaves on any GIT quotient of $V$ which is a scheme or more generally a Deligne-Mumford stack. Applications include:

  • Explicit combinatorial bases in the K-theory and cohomology of GIT quotients of this kind
  • Many new examples of derived equivalences between different Deligne-Mumford GIT quotients of linear representations of this kind
  • Fitting these derived equivalences together to form a representation of the fundamental group(oid) of the complexified Kaehler moduli space of the GIT quotient, and
  • Equivalences (under some mild hypotheses) between all Deligne-Mumford hyperkaehler quotients of a symplectic representation of a reductive group

"Combinatorial constructions of derived equivalences" with Steven Sam (arxiv:1601.02030)

Thumbnail
Equivariant Hodge theory and noncommutative geometry

We develop a version of Hodge theory for a large class of smooth cohomologically proper quotient stacks $X/G$ analogous to Hodge theory for smooth projective schemes. We show that the noncommutative Hodge-de Rham sequence for the category of equivariant coherent sheaves degenerates. This spectral sequence converges to the periodic cyclic homology, which we canonically identify with the topological equivariant $K$-theory of $X$ with respect to a maximal compact subgroup $M \subset G$. The result is a natural pure Hodge structure of weight $n$ on $K^n_M(X^{an})$. We also treat categories of matrix factorizations for equivariant Landau-Ginzburg models.

  • "Equivariant Hodge theory and noncommutative geometry" with Daniel Pomerleano (arxiv:1507.01924)
Thumbnail
Autoequivalences of derived categories and variation of GIT quotient

In geometric invariant theory (see below), the GIT quotient of $X/G$ depends on a choice from a continuous set of parameters. Nevertheless, the parameter space breaks down into "chambers" within which the GIT quotient does not vary, and these chambers are separated by "walls." When the parameters cross a wall, the GIT quotient is modified by a "birational transformation." I have been studying how the geometry and especially the derived geometry of the GIT quotient changes under such a wall crossing. For the special case of these wall crossings known as a "generalized flop," the derived geometry of the GIT quotient does not change at all. These cases are especially interesting -- they can reveal new symmetries of the derived category of the GIT quotient which do not arise in the classical geometry.

  • "Autoequivalences of derived categories and variation of GIT quotient," with Ian Shipman (arxiv:1303.5531)
Thumbnail
The derived category of a GIT quotient

If an algebraic group $G$ acts on an algebraic variety $X$, such as $\bC^\ast$ acting on affine space by dilation, is there a meaningful notion of a "space of orbits" for that action? Mumford's geometric invariant theory (GIT) answers this question by constructing a well-behaved orbit space for the action of $G$ on an open subset of "semistable points" of $X$. Many of the algebraic varieties we know and love (partial flag varieties, toric varieties,...) can be presented as GIT quotients of affine spaces. Since the 1980's, many beautiful relationships between the geometry and topology of the GIT quotient and the "equivariant" geometry of $X$ have been discovered. My research extends these relationships to the "derived" equivariant geometry of $X$ and the derived geometry of the GIT quotient.

  • The final version treats quotient stacks X/G subject to a certain technical hypothesis on the stratification (arxiv:1203.0276)
  • For newcomers, I'd recommend first looking at the version which treated just the smooth case (arxiv:1203.0276v2). Warning: This version contains some errors in the description of the stratification that I corrected in the final version.
  • Notes from an introductory talk

Machine Learning for Mathematics

Thumbnail
Learning selection strategies in Buchberger's algorithm

Studying the set of exact solutions of a system of polynomial equations largely depends on a single iterative algorithm, known as Buchberger's algorithm. Optimized versions of this algorithm are crucial for many computer algebra systems (e.g., Mathematica, Maple, Sage). We introduce a new approach to Buchberger's algorithm that uses reinforcement learning agents to perform S-pair selection, a key step in the algorithm. We then study how the difficulty of the problem depends on the choices of domain and distribution of polynomials, about which little is known. Finally, we train a policy model using proximal policy optimization (PPO) to learn S-pair selection strategies for random systems of binomial equations. In certain domains, the trained model outperforms state-of-the-art selection heuristics in total number of polynomial additions performed, which provides a proof-of-concept that recent developments in machine learning have the potential to improve performance of algorithms in symbolic computation.

  • "Learning selection strategies in Buchberger's algorithm" with Dylan Peifer and Mike Stillman (arXiv:2005.01917)
Thumbnail
Autoformalization for the working mathematician

This project is under development. With an interdisciplinary group of collaborators, I have designed a benchmark dataset that specifically targets a task that will be immediately useful for working mathematicians but is also challenging enough to be useful for machine learning researchers. Please email if you are interested in learning more or contributing.

The idea is that each datapoint will be a blueprint for the proof of a very challenging known result in research-level mathematics. The datapoint includes definition, lemma, and theorem statements in Lean4, and it includes proofs in natural language. The task is for the model to use the natural language arguments and the directed graph of logical dependencies between statements to fill in correct proofs in Lean4 for all missing proofs.

View Github Repo →

View Slides →

Thumbnail
Gold-medal-level IMO performance with automated formal theorem proving

I worked with the team at Harmonic.fun to develop their ``Aristotle" system to solve problems from the International Mathematical Olympiad. The system uses language models to do an enhanced tree search for proofs of lemma statements in Lean4. In July 2025, the system achieved a perfect score on 5 out of the 6 problems at IMO 2025, a gold-medal score. The system is still under development, but these results suggest that it has the potential to be a powerful tool for solving challenging mathematical problems.

View Blog Post →

Talks and expository writing

The Moduli Space (web book)

During the Spring 2020 term, I taught a graduate topics course on "Modern moduli theory," which I have reformatted into a web-based book.

We surveyed the theory of algebraic stacks (fibered categories and descent, quasi-coherent sheaves, quotient stacks, deformation theory, and Artin's criteria, Tannaka duality), then discussed more recent advances (the etale local structure theorems of Alper, Hall, and Rydh, and the results of beyond GIT), and applied these methods to the moduli of vector bundles and principal G bundles over a smooth curve.

Moduli of objects in dg-categories (2025)

Talk at Homological Mirror Symmetry conference in honor of Maxim Kontsevich's 60th birthday. I use recent results in moduli theory to give an intrinsic formulation of homological mirror symmetry, and I introduce some conjectures in symplectic topology that would imply it.

View Slides →

ICBS Talk (July 2024)

A proceedings paper On the structure of equivariant derived categories for the 2024 International Congress of Basic Science, based on my acceptance talk for a Frontiers of Science Award.

View Paper →

Swiss Lectures (2017)

Notes from lectures on Theta-stability and existence of good moduli spaces, with applications to Donaldson invariants.

Lecture 1 Lecture 2

Colloquium Talk (2017)

A colloquium-style slide talk on applications of beyond GIT to the D-equivalence conjecture.

View Slides →

AMS Proceedings (2015)

Proceedings paper for the AMS summer algebraic geometry institute (SLC, 2015).

Paper Video

Oberwolfach Report

Θ-reductive moduli problems, stratifications, and applications - Brief report from Oberwolfach workshop.

Read Report →

Graduate advising

I am currently accepting graduate advisees. If you are interested in working with me as your PhD advisor, please read my advising philosophy, which sets mutual expectations.

Recent Graduate Students

Dylan Peifer

PhD 2021

Professional Page →

Andres Fernandez-Herrero

PhD 2022

Professional Page →

Kimoi Kemboi

PhD 2023

Professional Page →

Trevor Jones

PhD 2025

Professional Page →

Alekos Robotis

PhD 2025

Professional Page →

Jeffrey Jiang

MS 2022

Sara Stephens

Current Student

Professional Page →
Photo

Mingjun Sun

Current Student

Professional Page →

Beyond geometric invariant theory concept map

One of the great challenges of research mathematics is effectively communicating mathematical ideas. In 2016, I created this concept map describing the "beyond GIT" project at the time. It needs updating, but it's a good starting point. Notably absent are the theorem on existence of good moduli spaces, and applications to the moduli of K-semistable Fano varieties.