SymPy prototype solves challenging integrals with few errors
Parallel Integration over Simple Radical Extensions in Mixed Towers: Charlwood's Integrals
Symbolic Computation
Summary
Integrating complicated math expressions can be very tricky. The authors tested a computer program in SymPy that tries to find these integrals automatically. It solved almost all of a set of 50 tough examples correctly, except one problem which they proved can’t be solved using simple math functions. Although their program is slower than some others, it is more accurate and shows where future speed improvements could be made.
What this means in practice
- •For computer algebra developers: Improve automatic integration modules by incorporating verified algorithms that handle complex radical expressions with fewer errors.
- •For scientific computing teams: Use verified integration methods to ensure correctness in symbolic computation within simulations or analytical tools involving complicated integrals.
Authors
Sam Blake
Abstract
We evaluate a SymPy implementation of the parallel Risch-Norman method using Charlwood's 2008 suite of 50 challenging indefinite integrals. The system automatically builds integrand towers, verifies answers by differentiation, and returns correct, verified integrals for 49 problems with zero errors. The single failure, $\int\arcsin(x\sqrt{1-x^2})\,dx$, is proven non-elementary using a holomorphic-remainder certificate, though limited by an unverified completeness hypothesis on a genus-three curve. Part II's degree bounds successfully reduce classical ansatz sizes by two-thirds without impacting running time. The paper details algorithmic mechanisms like $S'$-units, Pell units, and residue computing in tower coordinates. Compared to mature implementations, this untuned SymPy prototype is slower than FriCAS (by a factor of six on the median integral) but more accurate than AXIOM (which returned three wrong answers). Profiling pinpoints performance bottlenecks in nonlinear norm searches and nested number fields, outlining clear targets for optimisation.