SearcharxivSearch

arXiv subjects

Rushil Raghavan

Publications and source records attributed to Rushil Raghavan.

6 recordsLinked to original sources

From Solvers to Research: Large Language Model-Driven Formal Mathematics at the Research Frontier

Recent developments in AI for Mathematics (AI4Math), especially Large Language Model (LLM)-driven theorem provers, has achieved remarkable success in formal proof generation for well-defined mathematical problems through Interactive Theorem Proving (ITP) languages. However, current systems remain fundamentally limited in tackling frontier research mathematics, such as discovering new theorems or resolving open conjectures, which are often open-ended, under-specified, and involve multiple layers of abstraction. We argue that the next leap in AI4Math systems requires a decisive shift from predefined problem-solvers to research agents that can address frontier mathematical challenges with rigorous formal mathematical reasoning. In this position paper, we provide a systematic review of the field, covering datasets, auto-formalization, and proof synthesis. More importantly, we identify core limitations of existing systems in serving as mathematical research agents, examining issues across datasets, relational structure, mathematical exploration, tool ecosystem, and human-AI collaboration, outlining a strategic road-map for the future of AI4Math.

cs.CL

Improved Bounds for 3-Progressions

We prove that if $A\subset \{1,\dots,N\}$ has no nontrivial three-term arithmetic progressions, then $|A|\leq \exp(-c\log(N)^{1/6}\log\log(N)^{-1})N$ for some absolute constant $c>0$. To obtain this bound, we use an iterated variant of the sifting argument of Kelley and Meka, as well as an improved bootstrapping argument for Croot-Sisask almost-periodicity due to Bloom and Sisask.

math.NT

Improved Bounds for the Freiman-Ruzsa Theorem

Let $A$ be a finite subset of an abelian group $G$, and suppose that $|A+A|\leq K|A|$. We show that for any $\epsilon>0$, there exists a constant $C_\epsilon$ such that $A$ can be covered by at most $\exp(C_\epsilon \log(2K)^{1+\epsilon})$ translates of a convex coset progression with dimension at most $C_\epsilon \log(2K)^{1+\epsilon}$ and size at most $\exp(C_\epsilon \log(2K)^{1+\epsilon})|A|$. This falls just short of the Polynomial Freiman-Ruzsa conjecture, which asserts that this statement is true for $\epsilon=0$, and improves on results of Sanders and Konyagin, who showed that this statement is true for all $\epsilon>2$. To prove this result, we use a mixture of entropy methods and Fourier analysis.

math.NT

Sharp Bounds for Sets with Distinct Subset Products

Let $A\subseteq [N]$ be such that for any pair of distinct subsets $B,C\subset A$, the products $\prod_{b\in B}b$ and $\prod_{c\in C}c$ are distinct. We prove that $|A|\leq \pi(N)+\pi(N^{1/2})+o(\pi(N^{1/2}))$, where $\pi$ is the prime counting function, answering a question of Erd\H{o}s.

math.CO

Discordant sets and ergodic Ramsey theory

We explore the properties of non-piecewise syndetic sets with positive upper density, which we call "discordant", in countably infinite amenable (semi)groups. Sets of this kind are involved in many questions of Ramsey theory and manifest the difference in complexity between the classical van der Waerden's theorem and Szemer\'{e}di's theorem. We generalize and unify old constructions and obtain new results about these historically interesting sets. Along the way, we draw from various corners of mathematics, including classical Ramsey theory, ergodic theory, number theory, and topological and symbolic dynamics.

math.CO

Regular Isotopy Classes of Link Diagrams From Thompson's Groups

In 2014, Vaughan Jones developed a method to produce links from elements of Thompson's group $F$, and showed that all links arise this way. He also introduced a subgroup $\vec{F}$ of $F$ and a method to produce oriented links from elements of this subgroup. In 2018, Valeriano Aiello showed that all oriented links arise from this construction. We classify exactly those regular isotopy classes of links that arise from $F$, as well as exactly those regular isotopy classes of oriented links that arise from $\vec{F}$, answering a question asked by Jones in 2018.

math.GT