arXiv subjects

Brian Nugent

Publications and source records attributed to Brian Nugent.

6 recordsLinked to original sources

arXiv2026

Sorries Are Not the Hard Part: An Expert-Review Case Study of a Semi-Autonomous Formalization

Large language models can often close proof gaps in interactive theorem provers, but a verified theorem is not the same thing as a reusable library contribution. We study this distinction through a detailed case study: a semi-autonomous formalization of Grothendieck's vanishing theorem. The initial version compiles with no sorries, but an expert review found serious problems in definitions, theorem generality, file organization, and the API. We then ran a review-driven refactor and compression process and obtained a second expert review. The before-and-after comparison shows a sharp split: agents adapted well to local, mechanically checkable feedback, but remained weak at choosing definitions and designing APIs. We argue that autoformalization should be evaluated not only by closed sorries, but by whether the resulting formalization survives expert review.

cs.AI↗

arXiv2026

Higher Du Bois and Higher Rational Pairs

We extend the notions of higher Du Bois and higher rational singularities to pairs in the sense of the minimal model program. We extend numerous results to these higher pairs, including Bertini type theorems, stability under finite maps and that m-rational pairs are m-Du Bois. We prove these using a generalized Kovács-Schwede-type injectivity theorem for pairs, the main technical result of this paper.

math.AG↗

arXiv2025

Moduli of Very Ample Line Bundles

Let $X$ be a projective variety over a field. In this paper, we will construct a moduli space of very ample line bundles on $X$. In doing so, we develop a generalization of Fitting ideals to complexes of sheaves on $X$. We give other applications of these Fitting ideals such as constructing Brill-Noether spaces for higher dimensional varieties and giving a scheme structure to the locus where the projective dimension of a module jumps up.

math.AG↗

arXiv2022

Extending a problem of Pillai to Gaussian lines

Let $L$ be a primitive Gaussian line, that is, a line in the complex plane that contains two, and hence infinitely many, coprime Gaussian integers. We prove that there exists an integer $G_L$ such that for every integer $n\geq G_L$ there are infinitely many sequences of $n$ consecutive Gaussian integers on $L$ with the property that none of the Gaussian integers in the sequence is coprime to all the others. We also investigate the smallest integer $g_L$ such that $L$ contains a sequence of $g_L$ consecutive Gaussian integers with this property. We show that $g_L\neq G_L$ in general. Also, $g_L\geq 7$ for every Gaussian line $L$, and we give necessary and sufficient conditions for $g_L=7$ and describe infinitely many Gaussian lines with $g_L\geq 260,000$. We conjecture that both $g_L$ and $G_L$ can be arbitrarily large. Our results extend a well-known problem of Pillai from the rational integers to the Gaussian integers.

math.NT↗

arXiv2020

Walking to infinity on gaussian lines

We study analogies between the rational integers on the real line and the Gaussian integers on other lines in the complex plane. This includes a Gaussian analog of Bertrands Postulate, the Chinese Remainder Theorem, and the periodicity of divisibility. We also computationally investigate the distribution of Gaussian primes along these lines and leave the reader with several open problems.

math.NT↗

arXiv2018

Pure $\mathcal{O}$-sequences arising from $2$-dimensional PS ear-decomposable simplicial complexes

We show that the $h$-vector of a $2$-dimensional PS ear-decomposable simplicial complex is a pure $\mathcal{O}$-sequence. This provides a strengthening of Stanley's conjecture for matroid $h$-vectors in rank $3$. Our approach modifies the approach of combinatorial shifting for arbitrary simplicial complexes to the setting of $2$-dimensional PS ear-decomposable complexes, which allows us to greedily construct a corresponding pure multicomplex.

math.CO↗