arXiv subjects

Ashvni Narayanan

Publications and source records attributed to Ashvni Narayanan.

6 recordsLinked to original sources

arXiv2026

The Ramanujan Challenge For AI

To help evaluate the mathematical skills of current AI systems, we present a set of formulas for fundamental mathematical constants. These problems are attractive for AI evaluation because they are concrete and can be checked numerically to arbitrary precision, yet proving them may require non-obvious mathematics. Mathematical constants such as $π$, $e$, Catalan's constant, and special values of the Riemann zeta function have fascinated mathematicians for centuries. The search for formulas evaluating mathematical constants has produced some of the most beautiful mathematics in the field, especially in cases that yield irrationality proofs or fast convergence rates. Ramanujan's legacy is emblematic of this tradition. The list we provide contains two types of problems: formulas whose proofs are known to the authors but will remain encrypted for a short initial period; and formulas that are not yet proven. We are curious to see the achievements of AI in both cases.

math.HO↗

arXiv2025

Transformers know more than they can tell -- Learning the Collatz sequence

We investigate transformer prediction of long Collatz steps, a complex arithmetic function that maps odd integers to their distant successors in the Collatz sequence ( $u_{n+1}=u_n/2$ if $u_n$ is even, $u_{n+1}=(3u_n+1)/2$ if $u_n$ is odd). Model accuracy varies with the base used to encode input and output. It can be as high as $99.7\%$ for bases $24$ and $32$, and as low as $37$ and $25\%$ for bases $11$ and $3$. Yet, all models, no matter the base, follow a common learning pattern. As training proceeds, they learn a sequence of classes of inputs that share the same residual modulo $2^p$. Models achieve near-perfect accuracy on these classes, and less than $1\%$ for all other inputs. This maps to a mathematical property of Collatz sequences: the length of the loops involved in the computation of a long Collatz step can be deduced from the binary representation of its input. The learning pattern reflects the model learning to predict inputs associated with increasing loop lengths. An analysis of failure cases reveals that almost all model errors follow predictable patterns. Hallucination, a common feature of large language models, almost never happens. In over $90\%$ of failures, the model performs the correct calculation, but wrongly estimates loop lengths. Our observations give a full account of the algorithms learned by the models. They suggest that the difficulty of learning such complex arithmetic function lies in figuring the control structure of the computation -- the length of the loops. We believe that the approach outlined here, using mathematical problems as tools for understanding, explaining, and perhaps improving language models, can be applied to a broad range of problems and bear fruitful results.

cs.LG↗

arXiv2025

Learning Euler Factors of Elliptic Curves

We apply transformer models and feedforward neural networks to predict Frobenius traces $a_p$ from elliptic curves given other traces $a_q$. We train further models to predict $a_p \bmod 2$ from $a_q \bmod 2$, and cross-analysis such as $a_p \bmod 2$ from $a_q$. Our experiments reveal that these models achieve high accuracy, even in the absence of explicit number-theoretic tools like functional equations of $L$-functions. We also present partial interpretability findings.

math.NT↗

arXiv2023

Formalization of $p$-adic $L$-functions in Lean 3

The Euler--Riemann zeta function is a largely studied numbertheoretic object, and the birthplace of several conjectures, such as the Riemann Hypothesis. Different approaches are used to study it, including $p$-adic analysis : deriving information from $p$-adic zeta functions. A generalized version of $p$-adic zeta functions (Riemann zeta function) are $p$-adic $L$-functions (resp. Dirichlet $L$-functions). This paper describes formalization of $p$-adic $L$-functions in an interactive theorem prover Lean 3. Kubota--Leopoldt $p$-adic $L$-functions are meromorphic functions emerging from the special values they take at negative integers in terms of generalized Bernoulli numbers. They also take twisted values of the Dirichlet $L$-function at negative integers. This work has never been done before in any theorem prover. Our work is done with the support of \lean{mathlib} 3, one of Lean's mathematical libraries. It required formalization of a lot of associated topics, such as Dirichlet characters, Bernoulli polynomials etc. We formalize these first, then the definition of a $p$-adic $L$-function in terms of an integral with respect to the Bernoulli measure, proving that they take the required values at negative integers.

math.NT↗

arXiv2022

Towards a Mathematics Formalisation Assistant using Large Language Models

Mathematics formalisation is the task of writing mathematics (i.e., definitions, theorem statements, proofs) in natural language, as found in books and papers, into a formal language that can then be checked for correctness by a program. It is a thriving activity today, however formalisation remains cumbersome. In this paper, we explore the abilities of a large language model (Codex) to help with formalisation in the Lean theorem prover. We find that with careful input-dependent prompt selection and postprocessing, Codex is able to formalise short mathematical statements at undergrad level with nearly 75\% accuracy for $120$ theorem statements. For proofs quantitative analysis is infeasible and we undertake a detailed case study. We choose a diverse set of $13$ theorems at undergrad level with proofs that fit in two-three paragraphs. We show that with a new prompting strategy Codex can formalise these proofs in natural language with at least one out of twelve Codex completion being easy to repair into a complete proof. This is surprising as essentially no aligned data exists for formalised mathematics, particularly for proofs. These results suggest that large language models are a promising avenue towards fully or partially automating formalisation.

cs.CL↗

arXiv2022

A formalization of Dedekind domains and class groups of global fields

Dedekind domains and their class groups are notions in commutative algebra that are essential in algebraic number theory. We formalized these structures and several fundamental properties, including number theoretic finiteness results for class groups, in the Lean prover as part of the mathlib mathematical library. This paper describes the formalization process, noting the idioms we found useful in our development and mathlib's decentralized collaboration processes involved in this project.

cs.LO↗