Ramanujan Challenge Results: AI-Assisted Evaluation Pipeline for Multi-Format Proofs
Alan Sorani, Ashvni Narayanan, Michael Shalyt, Tali Monderer, Rotem Kalisch, Hila Barkan, Elyasheev Leibtag, Shachar Weinbaum 等 11 位作者
AI 速览：分析Ramanujan挑战赛提交，比较AI模型、CAS与形式化工具的表现，并提出一种评估自然语言证明、CAS代码与Lean形式化的AI辅助流水线。
As AI's mathematical capabilities rapidly improve, meaningful benchmarks are shifting from university-level problems and math olympiads to research-level mathematics. The Ramanujan Challenge is a benchmark comprised of research-level problems in number theory, including unpublished results and open conjectures. It presented concrete formulas for mathematical constants whose correctness can be checked numerically, while their proofs may require non-obvious mathematics. Here, we analyze the Challenge submissions, measuring the relative success of different AI models, Computer Algebra Systems (CAS), and formal tools. We find correct submissions that are conceptually distinct from the official solutions, and a proof of one of the published open conjectures. Evaluating the submissions exposed a second challenge: judging complex proofs reliably at scale. We introduce an AI-assisted evaluation pipeline for natural language proofs, CAS code, and Lean formalizations that assesses semantic and logical correctness. Compared with the conventional one-shot LLM judgment, our pipeline reduces false-positive verdicts on natural language proofs from 23% to 6% and improves judgment accuracy on supporting code from 46% to 58%. This approach provides a methodology for evaluating research-level mathematics at scale, with potential applications across mathematics and AI for science.
We examine whether the integers admit a topology whose connected subsets are precisely the sets of consecutive integers. The main result gives a construction for every integer lattice {\mathbb{Z}}^{n}, n>0; the answer for Z is then obtained as a corollary. We prove that the neighborhoods determined by the parity of the sum of the coordinates form a basis and that topological connectedness agrees exactly with accessibility by finite paths of unit lattice steps. We also present a deductive audit and the correspondence between this argument and a verification in Lean 4 and Mathlib, including the empty set and the independent formal characterization of integer intervals. The construction and mathematical result originate in Problem 5712, proposed by Dan Marcus and solved in 1970 by the Cleveland State University group; the present article contributes a detailed exposition and a report on formal verification.
Direct evaluation of the defining product of the Cayley-Dickson algebra $A_n$ of rank $N:=2^n$ over a unital commutative ring $R$ in which $2$ is invertible requires a quadratic number of arithmetic operations. This paper gives a uniform bilinear algorithm for multiplication in this algebra costing $O(N \log N)$ arithmetic operations in $R$ and $O(N)$ auxiliary storage when the doubling parameters of $A_n$ are units whose square roots lie in a fixed commutative coefficient algebra $S$ finitely generated as an $R$-module and admitting an $R$-linear map $π\colon S \to R$ with $π(1) = 1$. In particular, over $\mathbb{R}$ and every finite field $\mathbb{F}_{q}$ of odd characteristic, a quadratic field extension contains a square root of every possible doubling parameter, so the algorithm applies to every Cayley-Dickson tower over these fields, and the tensor rank of multiplication in $A_n$ over them is at most $(9n-21)2^n+28$ when $n\ge2$. When the top doubling parameter is a non-square, as in the standard real tower, the bound is $(9n-15)2^{n-1}+10$. To the author's knowledge, the algorithm presented in this paper is the first uniform subquadratic algorithm for multiplication in $A_n$. When $R=\mathbb{R}$ with every doubling parameter equal to $-1$, the real quasilinear schedule uses fewer total arithmetic operations than both direct multiplication and a uniform algorithm of Cariow-Cariowa for $n\ge4$. An implementation for the standard real tower is available in the MIT-licensed C11 library fastCD, with a NumPy-backed Python interface. In single-core benchmarks against direct multiplication and the uniform Cariow-Cariowa method, the quasilinear implementation had the lowest mean time of the three at every tested dimension $N\ge32$, for both single and batched products, and was over $17$ times faster than direct multiplication at $N=1024$.
Roberto La Scala, Marco Marchesin, Sharwan K. Tiwari
We investigate an algebraic approach to the Syndrome Decoding Problem, based on a reformulation of the Hamming weight constraint and its integration with the Information Set Decoding paradigm. We begin with a systematic analysis of the Hamming variety, deriving its defining equations in terms of elementary symmetric functions. Since these equations may have high degree, we exploit convolution identities for elementary symmetric functions, together with factorizations based on Lucas' identity, to derive an equivalent formulation with auxiliary variables and equations of bounded degree. Building on this modeling, we generalize the ISD paradigm through an ISD-like decoding strategy, implemented by the GBDecode algorithm, in which only a subset of an information set is fixed. This approach reduces the size of the combinatorial search space at the cost of solving the associated multivariate nonlinear systems. To handle this algebraic component, we employ the MultiSolve algorithm, which replaces a single Grobner basis computation with a collection of computations on simpler systems, obtained by exhaustively assigning a varying number of indeterminates over the finite field. This provides a tunable balance between combinatorial search and algebraic solving. We evaluate the resulting approach experimentally on instances of the Syndrome Decoding Problem for random binary linear codes, using parameters corresponding to the NIST Security Category 1 parameter set of the Classic McEliece cryptosystem. The experiments assess the feasibility of this combinatorial-algebraic approach and provide insights into the practical behavior of Grobner basis techniques within an ISD-like decoding framework.
We study the complexity of two fundamental problems attached to p-adic lattices: computing an N-orthogonal basis, and deciding whether a given basis is N-orthogonal. When the norm is supplied through an explicit diagonal representation, both problems are polynomial. However, in the black-box model, where the ultrametric norm N is fixed and only accessible through an evaluation oracle, we prove that both problems require $Ω$(p^{v-1} ) queries in the worst case, where v $\le$ n is the largest multiplicity of a commensurability class of N and n is the dimension of the ambient vector space. We then analyse the optimality of these bounds by providing explicit algorithms. Our results answer formally an open question of Zhang, Deng and Wang and refine the recent results of Duan and Wu by providing pointwise query bounds depending on the norm's structure, in addition to uniform bounds.
Systems of trigonometric equations appear frequently in problems related to geometry, kinematics, computer graphics, robotics, and astronomy, among many other fields. Most often these are first converted to algebraic equations via the ``tangent half-angle'' substitution and solved subsequently using various algebraic methods, such as computation of resultants. In the process, parametric singularities are introduced in the equations, and their degrees are also doubled. In this article, a novel concept call the ``Barik transform'' is introduced, which can help solve such a system without encumbering these issues, albeit only in systems that contain {\em at least} one equation of the first degree in the sine and cosine of the variable to be eliminated. It is shown how Barik transform can produce extremely compact eliminants in the closed form, without resorting to any resultant computation.
Automatic differentiation (the automatic computation of numerical function derivatives) has many applications, especially in scientific computing and machine learning. Several approaches to automate the calculation of derivatives have been presented. Common challenges facing those approaches include (1) having to define derivative rules for different classes of functions, (2) having to manipulate program symbols to understand the semantics of the function being differentiated, and construct the derivative function, and (3), more importantly, ensuring that the calculated derivative is correct. In this paper, we present an approach for automatic \emph{certified} differentiation using the Lean proof assistant. By certified, we mean a correctness certificate is computed together with the derivative function and a domain on which the derivative is guaranteed to be valid. Our approach leverages existing derivative theorems included in the Mathlib Lean library instead of having to define our own rules. We also utilize Lean metaprogramming to manipulate the symbolic structure of the input function, and to construct the derivative function. The correctness certificate is computed step-wise as we apply Mathlib theorems. To make the search efficient, we index the derivative theorems by the function they differentiate. We evaluate our approach on 500 randomly generated functions: with the index, all of them are differentiated, with a median time of 0.18\,s per function, 8.6 times faster than without the index.
Zeke Medley, Anagha Gokul, Quan Luu, Panagiotis Manolios
We present a GPU-accelerated algorithm for searching for ways to multiply matrices with few scalar multiplications. Our algorithm searches the matrix multiplication flip graph and, on an NVIDIA H200, performs over a billion search steps per second for matrix sizes up to $7\times7$, a roughly $380\times$ improvement over previous GPU-accelerated search on the tensor for $7\times7$ matrix multiplication. We also prove that, over \(\mathbb{F}_2\), the directed matrix multiplication flip graph is strongly connected with only flip and plus edges. This removes the need for computationally expensive reduction edges in the connectivity argument used by previous work. Using this GPU-accelerated search procedure on our simplified flip graph, we find a way to multiply $7\times 7$ matrices over $\mathbb{F}_2$ using 245 multiplications, a three-multiplication improvement over the previous record.
For masked rank-one least squares with unrestricted signs, gradients reveal weighted margins and the loss reveals the target's squared norm. We prove that this one scalar resolves the gradient ambiguity on bipartite cycle and length-three parallel-path blocks: every target fixed before sampling and nonzero on cycle edges is identified almost surely by one legal positive query drawn from an absolutely continuous law. On six-cycle flowers, open target and query sets retain $3^r$ bounded gradient candidates. A common algebraic witness excludes cross-block energy cancellation. Cactus masks admit explicit exception certificates and target-uniform finite-grid bounds; theta blocks admit an existence guarantee. For nondegenerate cactus reductions, an exact decoder returns complete actual real lists, with bit cost polynomial in input length, the cycle-degree product $D$ and the optional budget parameter $2^κ$. Energy-coordinate propagation certifies singletons without a product join. The product $D$ can grow exponentially in cycle count. Exponential certificate-degree and output bounds, and weak NP-hardness at a fixed uniform query, characterize distinct costs of exact decoding.
Engineers who audit a declared specification of an engineered system need to know which physical constraints it respects, which it violates, which field was altered and how to correct it. NeSySpec is an integrated and interpretable neuro-symbolic audit framework, built on Logic Tensor Networks, that answers these questions in one pipeline. Its axioms encode the physical relations of the domain as differentiable graded predicates whose tolerances are learned from a fleet of real records; from the same degrees, it diagnoses the violated constraint, identifies the altered field by abduction, proposes a minimum-change correction and ties image evidence to the parts it describes, abstaining exactly where evidence is missing, and returns all of it in one verification report. We validate NeSySpec on 107 aircraft types, with 16 test aircraft of 9 families held out of training, on specification records paired with ground photographs and satellite imagery and on synthetic errors: generated corruptions, edits labeled from the edit alone and deliberate falsifications. NeSySpec combines all the assessed audit outputs in one pipeline, which no learned, rule-based, solver-based, neuro-symbolic or language-model comparator does; on the test aircraft none is ahead of it in the macro-F1 of its constraint verdicts, in naming the violated constraint and the altered field or in the repair error, and it is competitive in record and image-pair detection. Its diagnosis names the violated constraint in 94.2% of corrupted test records, against 79.5% for classical Fellegi-Holt diagnosis, and on edits labeled from the edit alone, without retraining, abduction finds the altered field in 59.3% of records, against 30.6% for minimum-cardinality localization with random tie- breaking. Only the knowledge base, the visual predicates, the corruption generator and the data are specific to the domain.
Younes Naceur, Jie Wang, Victor Magron, Antonio Acín
Semidefinite relaxations of polynomial optimization have become a central tool for addressing the non-convex optimization problems over non-commutative operators that are ubiquitous in quantum information theory and, more in general, quantum physics. Yet, as these global relaxation methods are solved numerically, the bounds issued by the semidefinite solver can - and often do - exceed the global optimum, undermining their certifiability. To counter this issue, we introduce a framework for extracting rigorous certified bounds on non-commutative optimization problems from inexact numerical data, and apply it to several paradigmatic problems in quantum information theory. An extension to sparsity and symmetry-adapted semidefinite relaxations is also provided and compared to the general dense scheme. Our results establish rational post-processing as a practical route to reliable certification, pushing semidefinite optimization toward a certifiable standard for quantum information science.
Andrzej Indrzejczak, Tomasz Jarmu{ż}ek, Mateusz Klonowski, Michał Zawidzki
Non-Classical Logics. Theory and Applications (NCL) is an international conference aimed at presenting novel results and survey papers in the broad field of non-classical logics and their applications. The first two editions were held in Ł{ó}d{ź}, Poland, in September 2008 and 2009. Subsequent editions were organised in Toru{ń} (2010, 2012, 2015, 2018) and Ł{ó}d{ź} (2011, 2013, 2016, 2022, 2024). The tenth edition of the conference, organised by the University of Ł{ó}d{ź} in 2022, was the first to have its proceedings published in EPTCS. We are honoured and pleased to continue this practice and, for the third time, include all accepted long papers in an EPTCS volume. Furthermore, for the first time, we have also included all accepted extended abstracts in the volume.