Tyson Klingner

This paper gives a partial answer to a question of Dan Abramovich: consider a proper morphism \(f : \mathcal{X} \to \mathcal{Z}\) with connected fibers, between smooth separated Deligne--Mumford stacks, which defines an isomorphism away from a smooth effective Cartier divisor \(\mathcal{E} \subseteq \mathcal{X}\). Then, is \(f\) a weighted blowup? We confirm that \(f\) is an ordinary smooth blowup when \(\mathcal{X}\) and \(\mathcal{Z}\) are smooth separated schemes of finite type over \(\mathbb{C}\), and when \(f : \mathcal{X} \to \mathcal{Z}\) is a representable morphism of smooth separated Deligne--Mumford stacks. Further, we show that \(f\) is a weighted blowup when \(\mathcal{X}\) and \(\mathcal{Z}\) are smooth separated Deligne--Mumford surfaces, i.e., \(\dim \mathcal{X} = \dim \mathcal{Z} = 2\). As an application we determine when a reduction morphism between Hassett moduli stacks of weighted stable curves is given by a blowup along a smooth center.

We give a complete, self-contained computation of the spectral data parameterizing Higgs bundles in the generic fibers of the \(\mathrm{SO}_{2n+1}\)-Hitchin fibration where the Higgs fields are \(L\)-twisted endomorphisms. Although the spectral data is known in the literature, we develop a new approach, which takes advantage of Hecke modification. Further, we present the computation for the \(\mathrm{Sp}_{2n}\) and \(\mathrm{SO}_{2n}\) cases while clarifying some aspects of the correspondence which are not well explained in the pre-existing literature. We also compute the number of connected components of the generic fibers, and demonstrate Langlands duality in the fibers via the canonical duality in the fibers.

Within the past few years, the ability of Large Language Models (LLMs) to generate formal mathematical proofs has improved drastically. We provide a comparison of various LLMs' effectiveness in producing formal proofs in Lean 4 with the goal of assisting those seeking to use LLMs to support their own projects. We utilize both pass@\(k\) and refine@\(k\) metrics as the benchmark for our comparison and evaluate on subsets of both miniF2F and miniCTX datasets. Our testing shows that overall, Gemini 3.1 Pro and Claude Opus 4.7 perform best. Gemini 3.1 Pro achieved a 92% success rate on miniF2F via refine@32 whereas Opus 4.7 achieved a 86% success rate on miniCTX via refine@32. When taking cost into account, NVIDIA Nemotron 3 Super and GPT-OSS 120B were the most efficient, with competitive accuracies and average costs of \(<\$0.01\) per correct proof.