符号计算
We present a certified algorithm that takes a smooth algebraic curve in $\mathbb{R}^n$ and computes an isotopic approximation for a generic projection of the curve into $\mathbb{R}^2$. Our algorithm is designed for curves given implicitly…
A complete reduction on a difference field is a linear operator that enables one to decompose an element of the field as the sum of a summable part and a remainder such that the given element is summable if and only if the remainder is…
Wilf-Zeilberger pairs are fundamental in the algorithmic theory of Wilf and Zeilberger for computer-generated proofs of combinatorial identities. Wilf-Zeilberger forms are their high-dimensional generalizations, which can be used for…
We introduce beyond-worst-case analysis into symbolic computation. This is an extensive field which almost entirely relies on worst-case bit complexity, and we start from a basic problem in the field: isolating the real roots of univariate…
Though Mahler equations have been introduced nearly one century ago, the study of their solutions is still a fruitful topic for research. In particular, the Galois theory of Mahler equations has been the subject of many recent papers.…
In science, we are interested not only in forecasting but also in understanding how predictions are made, specifically what the interpretable underlying model looks like. Data-driven machine learning technology can significantly streamline…
In this contribution, we consider a zero-dimensional polynomial system in $n$ variables defined over a field $\mathbb{K}$. In the context of computing a Rational Univariate Representation (RUR) of its solutions, we address the problem of…
We present OSVAuto for automatic proofs about functional specifications that commonly arise when verifying operating system kernels. The algorithm behind OSVAuto is designed to support natively those data types that commonly occur in OS…
This paper demonstrates how certified computational tools can be used to address various problems in control theory. In particular, we introduce PACE.jl, a Julia package that implements symbolic elimination techniques, including (among…
We provide bounds on the size of polynomial differential equations obtained by executing closure properties for D-algebraic functions. While it is easy to obtain bounds on the order of these equations, it requires some more work to derive…
Moosbauer and Poole have recently shown that the multiplication of two $5\times 5$ matrices requires no more than 93 multiplications in the (possibly non-commutative) coefficient ring, and that the multiplication of two $6\times 6$ matrices…
These notes on creative telescoping are based on a series of lectures at the Institut Henri Poincare in November and December 2023.
Symbolic regression (SR) -- which learns symbolic equations to describe the underlying relation from input-output pairs -- is widely used for scientific discovery. However, a rich set of scientific data from the real world (e.g., particle…
Polyhedral affinoid algebras have been introduced by Einsiedler, Kapranov and Lind to connect rigid analytic geometry (analytic geometry over non-archimedean fields) and tropical geometry. In this article, we present a theory of Gr{\"o}bner…
The reason why Cooley-Tukey Fast Fourier Transform (FFT) over $\mathbb{Q}$ can be efficiently implemented using complex roots of unity is that the cyclotomic extensions of the completion $\mathbb{R}$ of $\mathbb{Q}$ are at most quadratic,…
This paper introduces a structured decoding framework for the Voynich Manuscript, based on mathematical rhythm, symbolic transformation, and glyph-level recursion. Rather than interpret symbols phonetically, this method decodes them by…
This paper presents a novel primality test based on the eigenvalue structure of circulant matrices constructed from roots of unity. We prove that an integer $n > 2$ is prime if and only if the minimal polynomial of the circulant matrix $C_n…
We identify a common scheme in several existing algorithms addressing computational problems on linear differential equations with polynomial coefficients. These algorithms reduce to computing a linear relation between vectors obtained as…
Ensuring software correctness remains a fundamental challenge in formal program verification. One promising approach relies on finding polynomial invariants for loops. Polynomial invariants are properties of a program loop that hold before…
Elaborating on an approach recently proposed by Mark van Hoeij, we continue to investigate why creative telescoping occasionally fails to find the minimal-order annihilating operator of a given definite sum or integral. We offer an…