Mathematical Sciences

► ImProver
Riyaz Ahuja

Advisors: Jeremy Avigad, Prasad Tetali, and Sean Welleck
Abstract: We present ImProver, a general-purpose agent-based framework and tool for Lean 4 proof optimization that enables templated and nontemplated neural theorem proving on arbitrary, user-defined metrics. Additionally, we define and analyze a set of metrics that are of general interest, including proof length, modularity, and readability, as well as a completion metric that enables nontemplated automated theorem proving. ImProver is powered by error-correction, tactic prediction, and example selection retrieval-augmented generation (RAG), as well as composite 15-sample refinement and best-of-n that promises output correctness. Additionally, we utilize Lean metaprogramming to extract proof state annotation information, as well as proof tree structure.

With this framework, ImProver outperforms SoTA language models (gpt-4o) on proof optimization tasks on undergraduate (MIL), competition (USAMO, IMO), and research-level (Polynomial Freiman-Ruzsa Conjecture) datasets with 57% mean metric improvement, 100% accuracy, and 54% nonzero accuracy -- compared to the baseline 19% improvement, 35.77% accuracy, and 15.33% nonzero accuracy.

► Mathematical Modeling of Micromagnetics
Nelitha Kulasiri, Henry Siegel, Michael Zhou

Advisor: Giovanni Leoni
Abstract: This research project investigates micromagnetics -- a theoretical framework developed by W.F.Brown, to describe the macroscopic behaviour of magnetic materials. A central concept in micromagnetics is the minimization of the magnetic energy within a material.

In this project we looked at the one dimensional variant of the energy equation: $E_{\varepsilon}(f) = \int_0^1 \varepsilon(f')^2 + \frac{1}{\varepsilon}|f^2-1|^{\alpha} dx$ . We separately analyzed the cases where $\alpha=1$, $\alpha=2$, and $1<\alpha<2$, and in all cases we found that the sequence of functions with minimized $E_{\varepsilon}$ was one which satisfies $f' = \frac{1}{\varepsilon}(1-f^2)^{\frac{1}{2}}$ up to an error factor, and explicitly found what the functions gamma converged to. For the $\alpha=1$ and $\alpha=2$ cases we found an explicit sequence.

We analyze the second order gamma of the function $G_\varepsilon(f) = \frac{E_{\varepsilon} - m_0}{h(\varepsilon)}$, where $h(\varepsilon)$ needed to be such that $G_{\varepsilon}$ had a nontrivial limit. For $\alpha=1$ and $\alpha=2$ we explicitly constructed an $h(\varepsilon)$ by finding the derivative of $E_{\varepsilon}$ with respect to $\varepsilon$ and using L'Hospital's theorem.

► Multivariate Gaussian Mixtures
Ishin Shah

Advisor: Tomasz Tkocz
Abstract: We study extremal-volume planar sections of unit balls in $\ell p$. Minimal-volume sections have been only recently found for the cross-polytope ($p=1$) via a geometric-analytic argument relying on convexity of certain functions arising from the radial function of a natural planar embedding of the sections. We have analysed several low-dimensional examples illustrating difficulties in extending this argument to the other values of $p$, beyond $p=1$. This analysis has enabled us to formulate a plausible conjecture for extremisers of cube slices (the case $p=\infty$).

► Representability of Polish groups on reflexive Banach spaces
Francesca Zhehan Yu

Advisor: Aristotelis Panagiotopoulos
Abstract: Given a group of symmetries G one often wants to know whether G can be understood through the ways in which it acts on a Hilbert space. In contrast to locally-compact topological groups, there are several Polish groups which admit no non-trivial (continuous) representation on a Hilbert space. Christensen and Herer provided one of the first examples of such an "exotic" group: the group of all real-valued measurable functions from the interval endowed with a pathological submeasure, endowed with the convergence in (sub)measure topology.

Through this project we explored whether the aforementioned topological group admits any interesting actions on more general classes of Banach spaces. Our preliminary findings suggest that it does not admit any non-trivial action by linear isometries on any reflexive Banach space either.

► Borel Complexity in Topology
Erica Assang, Thomas Kim, Daniel Mai

Advisor: Riley Thornton
Abstract: We can measure the complexity of a mathematical formula by counting alternating existential and universal quantifiers, and The Borel complexity of a set is the minimum quantifier complexity of a formula describing a set using only open predicates and quantifiers over countable sets. For instance the set of equivalence relations on $\mathbb{N}$ has complexity $\Pi^0_1$ since it can defined with only universal quantifiers, while the set of linear orders with a minimum is $\Sigma^0_2$ since it requires an ``exists" followed by a ``for all".

In this project, we analyzed the Borel complexity of several notions in topology.

We studied the set of Stone spaces with a given Cantor-Bendixson rank (a fundamental topological invariant measuring how densely packed a space's points are). We showed that the set of Stone spaces with Cantor--Bendixson rank $\alpha$ has complexity at most $\Pi_{2\alpha+4}$. And, we showed $\Pi_{2\alpha+2}$ is an upper bound on complexity if we restrict to countable spaces. We also prove that for finite $\alpha,$ $\Pi_{2\alpha+2}$ is a lower bound, and thus the Borel complexity of the set of countable spaces of finite Cantor--Bendixson rank is exactly $\Pi_{2\alpha+2}$. This project is ongoing and we expect to be able to extend these results to all $\alpha$ and establish a lower bound for the complexity of ranks for general Stone spaces.

We also analyzed various properties of subshifts-- topological spaces of functions equipped with a translation operation. We investigated topological entropy (a fundamental dynamical invariant measuring the information content in a subshift). And, we determined upper and lower bounds for the complexity of some fundamental subshifts.

► Anti-Ramsey Numbers for Regular Bipartite Graphs
Justin Blanco, Anna Deng, Joseph Wang

Advisor: Michael Young
Abstract: The anti-Ramsey number $AR(G, H)$ is the maximum value of $k$ such that there exists a $k$-coloring of edges in $G$ that does not contain any rainbow subgraph isomorphic to $H$, i.e. any copy of $H$ in $G$ contains at least 2 edges of the same color.

We explored anti-Ramsey problems in different types of graphs and proved the formula $$AR(B(n, d), nK_2) = d(n-2)+1$$ for $$n < \frac{d-2d^2+d^{2}n}{2-3d+2d^2},$$

where $B(n, d)$ is the $d$-regular bipartite graph with $n$ vertices in each part, and $nK_2$ is a perfect matching with $n$ edges.

► Accelerating NCE Convergence with Adaptive Normalizing Constant Computation
Sebastian Kumar, Wenyuan Shen

Advisor: Maria Chikina
Abstract: Noise Contrastive Estimation (NCE) is a widely used method for training generative models, typically used as an alternative to Maximum Likelihood Estimation (MLE) when exact computations of probability are hard. NCE trains generative models by discriminating between data and appropriately chosen noise distributions.

Although NCE is statistically consistent, it suffers from slow convergence and high variance when there is small overlap between the noise and data distributions. Both these problems are related to the flatness of the NCE loss landscape.

We propose an innovative approach to circumvent slow convergence rates by quick inference of the optimal normalizing constant at every gradient step. This allows the rest of the parameters to have more freedom during NCE optimization. We analyze the Bennett Acceptance Ratio (BAR) for quick computation of the normalizing constant and show improved performance for both methods on convex and non-convex settings. We prove that BAR converges to the right partition function under mild conditions of overlap. Using this we show an improvement in performance of BAR based on NCE over the vanilla baseline on the MNIST dataset.