Embedded Files
"It doesn't matter how long it takes, if the end result is a good theorem."
-John Tate
Research
My research lies at the intersection of algebraic geometry, arithmetic geometry, and algebra, with a central focus on rationality problems, algebraic tori, and toric geometry. Broadly, I study how cohomological and combinatorial methods classify algebraic structures and determine their rationality over arbitrary base fields. These questions trace back to some of the deepest ideas in algebraic geometry: understanding when varieties admit simple birational models, and how symmetries and group actions shape their classification. A recurring theme is the search for constructive frameworks that make these abstract relationships explicit, linking algebra, geometry, and arithmetic through concrete invariants.
A second strand of my work concerns formal verification and AI-assisted mathematics. I work in Lean 4 / Mathlib on formalizing research-level algebra, and on the question of whether machine-generated formalizations preserve the theorems they claim to state. The connection to the rest of my research is not incidental: both are about forcing mathematical content to be explicit enough to be checked
Publications/Preprints
On the Weak Lefschetz Property for Ideals Generated by Powers of General Linear Forms
(with Matthew Booth and Adela Vraciu)
Journal of Commutative Algebra
[link]
We describe the initial ideals of almost complete intersections generated by powers of general linear forms and prove that the Weak Lefschetz Property (WLP) in a fixed degree d holds when the number of variables n is sufficiently large relative to d. In particular, for ideals generated by squares, we determine precisely the range for which the WLP holds. Additionally, we provide bounds for the degree 3 case.
Classifying Torsors of Tori via Brauer Groups
(with Alexander Duncan)
Journal of Pure and Applied Algebra
[link]
Using Mackey functors, we develop a general framework for classifying torsors of algebraic tori in terms of Brauer groups of finite field extensions of the base field. This generalizes Blunk’s description of tori associated with degree 6 del Pezzo surfaces to all retract rational tori—essentially the largest class for which such a classification is possible.
Torsors of Generalized del Pezzo Tori and Brauer Groups (Submitted)
Using cohomological Mackey functors, we give an explicit Brauer group classification of torsors under tori of generalized del Pezzo varieties. This identifies the image of Lamarche's Brauer invariants and extends the Brauer-theoretic description in Blunk's classification of degree-six del Pezzo surfaces. We also determine which finite field extensions can appear in other Brauer group presentations of these torsors. The same tori act on Losev-Manin spaces, so the computation applies to these toric varieties as well.
Current Research
Auditing AI-Generated Lean 4 Formalizations (paper in preparation, slides available on request.)
This project will investigate the robustness of auto-formalization systems by identifying and characterizing their failure modes.
Formalizing Kontsevich Deformation Quantization in Lean 4.
Kontsevich's formality theorem produces a deformation quantization of any Poisson manifold, with the star product assembled from admissible graphs whose weights are integrals over configuration spaces, organized into an L∞-quasi-isomorphism. Formalizing it requires representing this graph combinatorics and the associated representation-theoretic structure inside Lean 4 in a form that supports the analytic estimates. This is a long-term collaborative formalization project, working on the graph-theoretic and algebraic components.
Weil explicit formula for the automorphic Langlands group and applications.
Explicit formulas in analytic number theory relate sums over zeros of L-functions to sums over primes, a correspondence that Weil recast in terms of the Weil group, the group carrying a canonical map with dense image to the absolute Galois group. This project takes up the analogous formula for automorphic L-functions expressed through the conjectural automorphic Langlands group, expected to be an extension of the Weil group, and works out its consequences assuming that group has its predicted properties. A natural application is to Sato Tate type equidistribution results for Frobenius elements and Satake parameters.
Twisted Forms of Losev–Manin Spaces and Arithmetic Invariants of Tori.
This project studies twisted forms of Losev–Manin spaces through algebraic tori, Brauer groups, and toric geometry. Building on my recent Brauer-group methods for torsors under tori, the aim is to determine when such twisted forms admit descriptions by explicit arithmetic invariants, connecting the geometry of toric compactifications to the classification of algebraic tori in low dimensions. The four-dimensional case is a particularly rich testing ground, where structural results on algebraic tori meet moduli-theoretic geometry.
Failure of the Weak Lefschetz Property for Powers of General Linear Forms.
This project investigates how the weak Lefschetz property fails for Artinian almost complete intersections generated by arbitrary powers of general linear forms, extending known sharp results for squares to generators of arbitrary degree. The central aim is to construct explicitly the elements responsible for the failure of maximal rank explicitly, generalizing the square case. The expected outcome is a more unified picture of Lefschetz behavior for almost complete intersections.
Future Goals
Proposed Research Directions
Advancing the Methodology for the Classification of Arbitrary Tori. Building on our published framework classifying all retract rational tori, I plan to extend the classification to arbitrary tori using elements of the Brauer group, giving a classification up to Brauer equivalence.
Mathlib Infrastructure for Algebraic Tori and Galois Cohomology. Mathlib's homological algebra for groups has advanced quickly: the bar resolution, long exact sequences, Shapiro's lemma, Hilbert 90, and now Tate cohomology in all integer degrees. What remains missing is the layer where the classification theory of tori lives: character lattices as Galois modules, permutation and flasque/coflasque resolutions, and the identification of the Brauer group of a field with a Galois cohomology group (Mathlib's Brauer group is currently the central-simple-algebra quotient, without the cohomological description). I want to build this. The statements I work with are unusually well suited to formalization: finitary, lattice-theoretic, and stated over arbitrary base fields, so they are easy to get subtly wrong by hand and correspondingly worth getting right mechanically.
Benchmarks for Research-Level Autoformalization. Existing formal benchmarks have begun reaching research difficulty, but they evaluate proving against a fixed, human-written formal statement. The complementary and largely unmeasured question is whether a model-produced formalization states the intended theorem at all, a proof can compile, use no sorry, and introduce no non-standard axioms while quietly proving something else. I want to develop difficulty-stratified benchmarks with human-adjudicated faithfulness labels, so that progress on research mathematics can be measured by whether the intended theorem was preserved rather than by whether the file builds.
Long-Term Vision
My long-term goal is to bridge algebraic geometry, non-commutative algebra, and Mackey functors toward a comprehensive classification of toric varieties over arbitrary fields, and to carry that classification into a proof assistant as it is developed rather than afterwards. A theory built on lattices, finite group actions, and cohomological invariants is one where formalization is genuinely tractable and where a formal library would be useful to others working on rationality problems, not merely a record of results already known. The two halves reinforce each other: formalizing forces every hypothesis to be explicit, which is exactly the discipline this subject demands.
Here are some further problems I am thinking about. If any of these directions catch your attention, I would be glad to collaborate.
How do Mackey and Tambara functors encode the birational geometry of G-varieties?
Can one classify equivariant contractions of del Pezzo and toric surfaces purely in Mackey functor terms?
What are the obstructions to G-rationality or stable G-rationality detectable from the functor data?
How do subgroup restrictions change the Mori cone, and can this be organized categorically?
Can we connect the representation theory of G with the structure of equivariant derived categories?
What is the right Lean representation of a character lattice with Galois action, such that flasque resolutions and the standard exact sequences are usable rather than merely definable?
Can the trivial-surrogate failure mode be detected automatically, for instance by testing whether a formalized statement remains provable after the key object is replaced by a canonical triviality?
Master's Thesis
Aug 2019 – June 2020
Master’s Thesis: Connectivity of the Tropical Double Ramification Cycle
Supervised by Dr. Dmitry Zakharov
Department of Mathematics, Central Michigan University, Mount Pleasant, MI, USA
My research investigated the connectivity properties of the tropical double ramification (DR) cycle, a polyhedral object in tropical geometry, within the moduli space of tropical curves of genus ggg with nnn marked points. Using graph-theoretic and combinatorial methods, I showed that the tropical DR cycle maintains connectivity in codimension one for specific parameter choices. This work integrates techniques from algebraic geometry, tropical geometry, and combinatorics, focusing on the construction and enumeration of cones in polyhedral spaces.
Expository Articles On Mackey Functors
These notes were created to facilitate my understanding of Mackey functors at the onset of my project. They serve as an introductory resource for those interested in the topic.
Theory_Of_Cohomological_Mackey_Functors.pdfPage updated
Google Sites
Report abuse