ALT The 2022–2026 burst of activity in small-format matrix multiplication (AlphaTensor 2022, AlphaEvolve 2025, Schwartz–Zwecher 2025) has produced striking individual results but scattered them across different fields, attribution conventions, and serialisation formats. A complementary line of work – Perminov's open-source flip-graph framework – instead drives existing construction methods, notably flip-graph and meta-flip-graph search, at scale across large format spaces, discovering many new low-rank schemes (including ternary-integer ones) that further enrich the landscape this catalog must unify. We present a unified, machine-checkable catalog covering shapes up to nmpshape323232 over Rationals, Integers, Reals, Complex, and Ftwo, with a separate axis for commutative algorithms (Waksman 1970, Makarov 1986, Rosowski 2019). Derivation over this catalog is performed by a frontier-closure search that recombines catalog entries by axis-flip, Kronecker, axis concatenation, serendipitous prod

ALT In this paper, we prove that output-sensitive sparse polynomial GCD computation over finite fields is NP-hard under BPP many-one reduction. More precisely, for two sparse univariate polynomials f,g with finite field coefficients, there exists no randomized algorithm to compute gcd(f,g), which is polynomial-time in the sizes of f,g,\gcd(f,g) under the standard complexity assumption NPnsubseteqBPP. This settles the open problem posed as Challenge 5 in The Sparsity Challenges in the finite field setting. Furthermore, we show that the Roots of Unity Detection problem over finite fields is NP-hard; that is, determining whether the GCD of a sparse univariate polynomial and x^n - 1 has nonzero degree is NP-hard.

ALT In this paper, we show that deciding whether a sparse polynomial does not divide another sparse polynomial exactly over finite fields is NP-hard under BPP many-one reductions. Equivalently, the sparse polynomial divisibility test over finite fields is CoNP-hard. This resolves the long-standing open problem concerning the computational complexity of the divisibility test for sparse polynomials in the setting of finite fields.

ALT Sparse polynomial multiplication is a fundamental problem in computer algebra and the theory of computation, and the development of a quasi-linear time output-sensitive multiplication algorithm has been posed as an open challenge. In this paper, a counterexample is provided to a previously claimed solution to this open problem for integer coefficients. By employing the existing quasi-linear modular-black-box interpolation algorithm, we are able to provide an algorithm with quasi-linear bit complexity for the integer coefficients setting. Furthermore, in the case of coefficients over a finite field, we obtain an algorithm whose bit complexity is linear in the number of terms, the logarithm of the degree, and the logarithm of the size of the finite field.

ALT We prove the positive-real n=9 case of the Vasc cyclic inequality. The proof was obtained with human-guided assistance from the AI agent MechMath Agent Team: the human-readable part reduces the rational inequality to a homogeneous polynomial inequality, fixes a cyclic maximum, and parametrizes each sorted fixed-maximum cone by cumulative gaps; the finite part is a certificate covering all 8!=40320 sorted cones. MechMath Agent Team generated the certificate verification workflow through Python tool calls, including the case split, verification programs, and terminal classifications. The published certificate has 36815 coefficient leaves, 2236 ordinary Polya multiplier leaves, and 1269 AM-GM midpoint overlay leaves. Human authors audited the mathematical reductions and verification logic, and a separate artifact contains the certificate, an independent verifier, and a from-source rebuild route.

ALT This paper presents new results for fast matrix multiplication in small formats obtained by combining the meta flip graph framework with the serendipitous product construction. The framework has been extended to support all 680 rectangular formats with dimensions up to 16 × 16 × 16. Compared to the previous state of the art, ranks are improved for 206 formats. For 84 formats, ternary schemes are found where previously only integer or rational coefficients were known. Additionally, 23 new schemes with asymptotic exponent ω< log₂ 7 are discovered, bringing the total number of such schemes to 52. The overall distribution of coefficient types across all investigated formats is 375 ternary, 18 integer, and 287 rational. All code and discovered schemes are available as open source.

ALT Large Language Models (LLMs) have demonstrated impressive progress in complex reasoning tasks, largely driven by the Chain-of-Thought (CoT) paradigm, which decomposes difficult problems into intermediate steps. However, CoT reasoning remains fundamentally constrained by the probabilistic nature of neural generation, leading to unfaithful reasoning chains that undermine reliability. Neuro-symbolic approaches attempt to address these issues by combining LLMs with symbolic solvers, yet they face persistent challenges, including hallucinated translations, the mismatch between natural language and formal logic, and the limited enhancement of the LLM's intrinsic reasoning ability. To overcome these limitations, we propose Symbolic-Neural Soft-Logic Reasoning (SSR), a unified framework that integrates LLMs with symbolic reasoning and improves robustness by relaxing strict logical determinism while preserving verifiability. Our approach improves reasoning performance, automatically generates v

ALT We study the problem of computing the isolated regular solutions of a system (f₁,…,fₙ) of n polynomial equations in n variables (X₁, …, Xₙ) over a field of characteristic zero k. We focus on systems with a composable structure, where each polynomial fᵢ can be expressed as a composition fᵢ = hᵢ(g₁,…,gₙ). Exploiting this structure allows us to reduce the original system to one in the gⱼ variables, thereby significantly improving the efficiency of symbolic solution algorithms. We present a probabilistic algorithm that computes all isolated regular solutions, with arithmetic complexity being polynomial in the input size and in the number of solutions. A first important application is when f₁, …, fₙ belong to the subring k[g₁, …, gₙ], where g₁, …, gₙ are algebraically independent polynomials in k[X₁, …, Xₙ]. Another important application is to systems of invariant polynomials under finite reflection groups, since by the Chevalley-Shephard-Todd theorem their invariant rings are polynomial al

ALT A new symbolic algorithm to compute sums of squares multipliers (certificates) to witness the membership of non-negative univariate polynomials in a saturated univariate quadratic module is presented. Certificates are first computed in terms of natural generators introduced by Kuhlmann and Marshall for an Archimedean saturated quadratic module; natural generators can be easily read-off from a semialgebraic set. In the univariate case, an Archimedean quadratic module is also a preordering since it is closed under multiplication; certificates have different representations when a polynomial is viewed as a member in a quadratic module versus in a preordering An algorithm is given to compute certificates of natural generators in terms of the original generators; it uses a construction introduced by Kuhlmann, Marshall, and Schwartz known as the “Basic Lemma”, which splits the non-negative factors of generators. To compute a quadratic module certificate, certificates of products of natural g

ALT We consider the problem of computing sample points in each connected component of a semi-algebraic set defined by the non-vanishing or the positivity of an n-variate polynomial of degree d, with rational coefficients of bit size bounded by τ. Such a problem is a basic routine in effective real algebraic geometry, used in higher-level algorithms for solving polynomial systems over the reals and finds many applications in sciences. We design a probabilistic algorithm for solving this problem, which is based on reductions to different routines for solving zero-dimensional polynomial systems. It assumes that the input polynomial satisfies sufficiently generic properties (namely, smoothness of its defining hypersurface). This is done through the computations of critical points of well-chosen maps to capture the connected components of the semi-algebraic set under study. We derive a bit complexity estimate for the cost of this algorithm, which is, in terms of the Bézout bound d(d -1)ⁿ⁻¹, ess

ALT A fundamental challenge in symbolic regression (SR) is efficiently recovering complex mathematical expressions from observational data. Although this problem is NP-hard, many expressions of practical interest decompose naturally into combinations of nonlinear feature modules, concentrating structural complexity into a small number of reusable components. Here, we introduce FePySR, a two-stage framework that reduces the SR search space by extracting valid features prior to equation search. FePySR first employs a heterogeneous neural network to constrain observational data to a set of candidate expressions, then performs structural optimization within this refined expression space using PySR. Across five standard benchmarks, FePySR outperforms state-of-the-art methods by achieving higher equation recovery rates. On a set of 75 highly complex synthesized equations, FePySR recovers 36 equations, while producing substantially smaller mean squared errors on the remaining unrecovered cases, w

ALT When a computer algebra system fails to solve an Ordinary Differential Equation, is this a limitation of its implementation, or a genuine computational barrier? Three traditions bear on the question. Modern computer algebra algorithms can be extremely efficient: Newton-type methods solve polynomial ODEs over ℚ[[X]] in quasi-linear time. Analog models of computation has shown that polynomial ODEs and Turing machines are two presentations of the same phenomenon, with solution length acting as time and precision as space. Computable analysis shows that ODEs can be intrinsically hard – undecidable, even PSPACE-complete, over compact domains. Comparing these traditions is natural and necessary, yet such comparisons routinely reduce to comparisons of encodings rather than of underlying algorithmic content. We argue that reverse mathematics provides a representation-invariant lens in which algorithmic content is compared directly. We prove that every level of the Big Five hierarchy is inhabit

ALT We introduce Exhaustive Symbolic Integration (ESI), a method that enumerates all symbolic functions up to a given complexity k within a specified operator basis and determines which admit closed-form antiderivatives within the same class. This allows us to compute the "integrability fraction" ρ(k) (the fraction of functions whose derivatives lie within the same class), which we do for five operator bases including combinations of rational functions, powers, exponentials, logarithms and trigonometric functions. We find that ρ(k) declines at high complexity and that the operator basis has a dramatic effect – in particular, adding the logarithm boosts ρ(k) by a factor of ∼3 and produces or exacerbates a clear peak at k=6. We also deploy ESI as a novel integration algorithm, identifying three integrals that resist SymPy, Mathematica, RUBI, FriCAS, Maxima and Giac under all tested strategies. When an antiderivative can be found by multiple methods, ESI often returns the simplest form. These

ALT Cylindrical Algebraic Decomposition (CAD) algorithms typically produce a decomposition adapted to a finite family of semi-algebraic sets ℱ (i.e. every member of ℱ is a union of cells). Different algorithms may produce different outputs, and introduce unnecessary cell divisions. Recent work by Michel, Mathonet, and Zénaïdi in ISSAC 2024 formalised this issue by studying the refinement order on the set of all CADs adapted to ℱ and analysing the existence of a minimum (coarsest) adapted CAD. It was shown that such a minimum adapted CAD always exists for subsets of ℝ and ℝ², but not of ℝⁿ (n ≥slant 3) in general. It is natural to seek natural classes of subsets of ℝⁿ that admit a minimum adapted CAD. In this paper, we identify a class of subsets of ℝ³ that contains all algebraic sets for which minimum adapted CADs do exist. This provides the first positive existence theorem for minimum CAD for a non-trivial class of sets.

ALT This paper focuses on asymptotic properties of random monomial ideals through a statistical viewpoint. It extends the study of redundancy in monomial ideals by analyzing the poset density of the LCM-lattice. We explore how this density behaves across random algebraic models and structured networks. Experimental data reveal that the LCM-lattice exhibits sharp threshold behavior rather than changing smoothly. We observe a strong negative correlation between the number of generators and LCM-lattice density, abruptly separating three distinct regimes: a low-density Taylor-like regime, a high-density redundant regime, and a narrow transition window. We show that increasing the generator degree causes this density drop to occur at lower probability thresholds. We conclude by conjecturing that for equigenerated squarefree ideals, the LCM-lattice density undergoes a sharp phase transition, analogous to the emergence of giant components in hypergraphs. This suggests that the classical, ideal-by

ALT We give a self-contained, modern exposition of Édouard Goursat's 1887 theorem on pseudo-elliptic integrals – those integrals of the form ∫ F(t) ṭ/√R(t) with R a cubic or quartic polynomial that, despite living on a genus-1 algebraic curve, admit elementary antiderivatives. After reviewing integration in finite terms and Liouville's theorem, we present Goursat's two main theorems with proofs phrased in the language of Möbius automorphisms of the underlying hyperelliptic curve. We then develop a cube-root analog: for integrals of the form ∫ F(t) ṭ/√[3]R(t) with R cubic, an order-3 Möbius substitution cyclically permuting the roots of R induces an eigendecomposition into three pieces. Two of the three eigenpieces (eigenvalues 1 and ω², where ω=e²πⁱ/³) descend through a chain of substitutions to genus-0 curves and yield elementary antiderivatives; the middle eigenpiece (eigenvalue ω) descends only to the genus-1 curve y³ = x(x-K) and is generically transcendental.

ALT We describe the design of a quantifier elimination framework for the complex numbers in the language of ordered rings supplemented with symbols for the imaginary unit, real parts, imaginary parts, and conjugates. Technically, we use a reduction to real quantifier elimination followed by a heuristic reinterpretation of the results within our complex framework. We present computational examples using a prototypical implementation of our approach in our Python-based open-source system Logic1.

ALT We design the Arboretum.hs package for symbolic computations with algebras of trees and more general graphs in Haskell. Thanks to the declarative nature of functional programming, the package's implementation closely follows mathematical definitions, making the code intuitive and transparent for users working with algebraic and combinatorial structures. To assist with current mathematical research, Arboretum.hs supports experimentation by facilitating the introduction of new algebraic operations, as well as providing functionality for rendering trees and forests through LaTeX integration. Compared to recent imperative implementations in languages such as Julia or Python, Arboretum.hs offers greater flexibility for manipulating and extending tree-based structures. Its use of Haskell enables safe programming and strong compile-time guarantees, serving both as a practical computational tool and a foundation for further research in algebraic combinatorics, beyond the setting of trees usual

ALT Equivalence checking of quantum circuits is a central verification task in quantum computing, ensuring the correctness of circuit optimizations, hardware mappings, and compilation pipelines. Among the primary symbolic methods for this purpose, the path-sum formalism provides a compact representation with powerful reduction rules that yield a canonical form for the classically simulable Clifford fragment, but confluence fails beyond the Clifford fragment. We introduce a new weighted model counting (WMC) encoding for path-sums and combine it with the existing path-sum reductions to obtain a verifier that is both complete and efficient. Our method applies reductions whenever possible and invokes the WMC-based decision procedure on the residual path-sum, yielding a complete semantic check up to a global phase. We implement the approach and evaluate it on standard benchmarks. Results show that the hybrid method outperforms either component in isolation and competes with state-of-the-art too

ALT This paper presents two enhancements to cylindrical algebraic decomposition (CAD) based quantifier elimination (QE) for cases in which multiple equational constraints are present in the given input formula φ. The first enhancement provides more detail in the output when there is a conceptual partition of the set of variables of φ into parameters and unknowns. In such cases, we describe how to partition the parameter space so that: (1) in each open set of the partition the number ν of associated unknowns is a finite constant or is infinite; and (2) for each such open set for which ν is finite, an expression for the unknowns in terms of the parameters is provided. The second enhancement is an efficiency gain achievable in certain situations. Indeed, when certain conditions are met, the second CAD equational projection step can be reduced more significantly than is supported by the prior existing theory. Relevant theorems and worked examples for both enhancements are provided. Application