arXiv subjects
Publications and source records attributed to Giovanni Inchiostro.
We introduce a new stability condition for log Calabi--Yau fibrations over curves. We prove that it gives rise to a proper Deligne--Mumford stack with a projective coarse moduli space, whose boundary still parametrizes flat fibrations over curves.
Mathematical knowledge is organized around statements and their dependencies, but this structure is exposed unevenly: informal papers cite mostly at the document level, while formal libraries record fine-grained dependencies over a much smaller body of mathematics. We introduce TheoremGraph, a unified statement-level dependency graph spanning both informal and formal mathematics. On the informal side, we parse 11.7M theorem-like environments from mathematics arXiv and recover 18.3M candidate directed dependencies, each labeled by the extractor that proposed it so downstream users can trade coverage for precision. On the formal side, we release LeanGraph, a Lean 4 elaborator-level extractor producing 388,105 declaration nodes and 11.3M typed edges across 25 Lean projects. We bridge the two graphs by embedding generated natural-language slogans into a shared semantic space, linking related statements across papers and across the informal/formal divide; an LLM judge affirms 47,952 such matches above a 0.8 cosine floor, with the judge-acceptance rate rising from 48% across the floor to 87% in the >=0.9 tier. On formal concept retrieval, our name-and-signature representation with graph expansion comes within 0.5pp of LeanSearch v2's reranked Recall@10 (0.775 vs. 0.780) without an LM reranker. We release the dataset, extractors, HTTP API, and MCP interface as infrastructure for mathematical search, attribution, and retrieval-augmented reasoning, available at theoremsearch.com and huggingface.co/datasets/uw-math-ai/theorem-matching.
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.
Searching for mathematical results remains difficult: most existing tools retrieve entire papers, while mathematicians and theorem-proving agents often seek a specific theorem, lemma, or proposition that answers a query. While semantic search has seen rapid progress, its behavior on large, highly technical corpora such as research-level mathematical theorems remains poorly understood. In this work, we introduce and study semantic theorem retrieval at scale over a unified corpus of $9.2$ million theorem statements extracted from arXiv and seven other sources, representing the largest publicly available corpus of human-authored, research-level theorems. We represent each theorem with a short natural-language description as a retrieval representation and systematically analyze how representation context, language model choice, embedding model, and prompting strategy affect retrieval quality. On a curated evaluation set of theorem-search queries written by professional mathematicians, our approach substantially improves both theorem-level and paper-level retrieval compared to existing baselines, demonstrating that semantic theorem search is feasible and effective at web scale. The project page, search tool, dataset, REST API, and MCP server are available at theoremsearch.com.
This paper continues the study initiated in [ISZ25] on the moduli of surfaces admitting lc-trivial fibrations. Using the techniques developed in [ISZ25], we (1) provide a classification of the surfaces appearing on the boundary of the KSBA-moduli space of elliptic surfaces with a bisection (2) recover the results of a series of papers on the moduli stacks of elliptic surfaces with a section [AB22, Inc20, Bru15]. Notably, our proof of (2) avoids the use of explicit steps of an MMP, such as the "La Nave flip" from [LN02], which plays a central role in [AB22,Inc20]. As an application, we compactify the moduli stack of hyperelliptic K3 surfaces.
We study the moduli spaces of surface pairs $(X,D)$ admitting a log Calabi--Yau fibration $(X,D) \to C$. We develop a series of results on stable reduction and apply them to give an explicit description of the boundary of the KSBA compactification. Three interesting cases where our results apply are: (1) divisors on $\mathbb{P}^1 \times \mathbb{P}^1$ of bidegree $(2n,m)$; (2) K3 surfaces which map $2:1$ to $\mathbb{F}_n$, with $X=\mathbb{F}_n$ and $D$ the ramification locus, or (3) elliptic surfaces with either a section or a bisection. The main tools employed are stable quasimaps, the canonical bundle formula, and the minimal model program.
We prove a root stack valuative criterion for good moduli space maps and for gerbes for reductive groups under some mild assumptions on the residue characteristic. We give several applications to parahoric extension for torsors, rational points on stacks, gerbes and homogeneous spaces, and the geometry of fibrations.
We compactify moduli stacks of maps from curves to a large class of quotient stacks $[W/G]$ admitting projective good moduli spaces. Our construction extends quasimap-theoretic compactifications and relies on a new birational operation for algebraic stacks, which we call an extended weighted blow-up. As applications, we construct compactifications of certain moduli spaces of fibrations in log Calabi-Yau pairs, of maps to stacks of the form $[W/\mathbb{G}_m^n]$, of maps to the GIT moduli stack of $2n$ points on $\mathbb{P}^1$, and of maps to the GIT moduli stack of plane cubics. In the appendix, we use extended weighted blow-ups to give a modular proof of a conjecture of Hassett.
In this article, we construct an infinite sequence of irreducible components of Koll\'{a}r--Shepherd-Barron (KSB-) moduli spaces of surfaces of arbitrarily large volumes, and describe the boundary of each component completely. Moreover, we describe the stable reduction steps in finding the KSB-limits in an explicit combinatorial way. Our main approach is to study the moduli spaces of elliptic surfaces with Kodaira dimension one, fibered over rational curves, using the techniques of wall-crossing for KSBA moduli and twisted stable maps.
We establish a criterion for determining when a smooth Deligne-Mumford stack is a weighted blow-up. More precisely, given a smooth Deligne-Mumford stack $\mathcal{X}$ and a Cartier divisor $\mathcal{E} \subset \mathcal{X}$ such that (1) $\mathcal{E}$ is a weighted projective bundle over a smooth Deligne-Mumford stack $\mathcal{Y}$ and (2) for every $y\in\mathcal{Y}$ we have $\mathcal{O}_{\mathcal{X}}(\mathcal{E})|_{\mathcal{E}_y}\simeq \mathcal{O}_{\mathcal{E}_y}(-1)$, then there exists a contraction $\mathcal{X}\to\mathcal{Z}$ to a smooth Deligne-Mumford stack $\mathcal{Z}$. Moreover, the stack $\mathcal{X}$ can be recovered as a weighted blow-up along $\mathcal{Y}\subset \mathcal{Z}$ with exceptional divisor $\mathcal{E}$, and $\mathcal{Z}$ is a pushout in the category of algebraic stacks. As an application, we show that the moduli stack $\overline{\mathscr{M}}_{1,n}$ of stable $n$-pointed genus one curves is a weighted blow-up of the stack of pseudo-stable curves. Along the way we also prove a reconstruction result for smooth Deligne-Mumford stacks that is of independent interest.
We develop the moduli theory of boundary polarized CY pairs, which are slc Calabi-Yau pairs $(X,D)$ such that $D$ is ample. The motivation for studying this moduli problem is to construct a moduli space at the Calabi-Yau wall interpolating between certain K-moduli and KSBA moduli spaces. We prove that the moduli stack of boundary polarized CY pairs is S-complete, $\Theta$-reductive, and satisfies the existence part of the valuative criterion for properness, which are steps towards constructing a proper moduli space. A key obstacle in this theory is that the irreducible components of the moduli stack are not in general of finite type. Despite this issue, in the case of pairs $(X,D)$ where $X$ is a degeneration of $\mathbb{P}^2$, we construct a projective moduli space on which the Hodge line bundle is ample. As a consequence, we complete the proof of a conjecture of Prokhorov and Shokurov in relative dimension two.
We give a valuative criterion for when a smooth algebraic stack with a separated good moduli space is the quotient of a separated Deligne-Mumford stack by a torus. For doing so, we introduce a new class of morphisms, the so-called effective morphisms, which are a generalization of separated morphisms.
We give a definition of twisted map to a quotient stack with projective good moduli space, and we show that the resulting functor satisfies the existence part of the valuative criterion for properness.
Associated to a convex integral polygon $N$ in the plane are two integrable systems: the cluster integrable system of Goncharov and Kenyon, constructed from the dimer model on bipartite torus graphs, and the Beauville integrable system associated with the toric surface of $N$. These two systems are related by a birational map called the spectral transform. In this paper we study the case when $N$ is the standard triangle of side length $d$, equivalently when the toric surface is $\P^2$, and prove that the spectral transform is a birational isomorphism of integrable systems. Since the Hamiltonians are identified by construction, the essential content is that the spectral transform intertwines the two Poisson structures. In particular, this shows that Beauville integrable systems admit cluster algebra structures.
We compute the Chow rings with integral coefficients of moduli stacks of minimal Weierstrass fibrations over the projective line. For each integer $N\geq 1$, there is a moduli stack $\mathcal{W}^{\mathrm{min}}_N$ parametrizing minimal Weierstrass fibrations with fundamental invariant $N$. Following work of Miranda and Park--Schmitt, we give a quotient stack presentation for each $\mathcal{W}^{\mathrm{min}}_N$. Using these presentations and equivariant intersection theory, we determine a complete set of generators and relations for each of the Chow rings. For the cases $N=1$ (respectively, $N=2$), parametrizing rational (respectively, K3) elliptic surfaces, we give a more explicit computation of the relations.
Associated to a convex integral polygon $N$ is a cluster integrable system $\mathcal X_N$ constructed from the dimer model. We compute the group $G_N$ of symmetries of $\mathcal X_N$, called the (2-2) cluster modular group, showing that it is a certain abelian group conjectured by Fock and Marshakov. Combinatorially, non-torsion elements of $G_N$ are ways of shuffling the underlying bipartite graph, generalizing domino-shuffling. Algebro-geometrically, $G_N$ is a subgroup of the Picard group of a certain algebraic surface associated to $N$.
We give an explicit description of $\overline{\mathcal{M}}_{1,2}$ as a weighted blow-up of a weighted projective stack. We use this description to compute the Brauer group of $\overline{\mathcal{M}}_{1,2;S}$ over any base scheme $S$ where 6 is invertible, and the integral Chow rings of $\overline{\mathcal{M}}_{1,2}$ and $\mathcal{M}_{1,2}$.
We develop a framework to construct moduli spaces of $\mathbb{Q}$-Gorenstein pairs. To do so, we fix certain invariants; these choices are encoded in the notion of $\mathbb{Q}$-stable pair. We show that these choices give a proper moduli space with projective coarse moduli space and they prevent some pathologies of the moduli space of stable pairs when the coefficients are smaller than $\frac{1}{2}$. Lastly, we apply this machinery to provide an alternative proof of the projectivity of the moduli space of stable pairs.