Algorithmic Discovery of Algebraic Identities: A Survey (Seven Decades)

The automation of mathematical discovery represents one of the most profound applications of computer science to pure mathematics. From Sister Celine's 1945 thesis to Google DeepMind's 2024 FunSearch, researchers have developed increasingly powerful algorithms that discover, prove, and even conjecture new algebraic identities—transforming what was once artisanal mathematical craft into systematic computational science. This report surveys seven decades of work across classical algorithmic methods, computer algebra implementations, modern machine learning approaches, and automated conjecture systems.

Classical algorithms established the algorithmic foundations

The modern era of computerized identity proving began with Sister Mary Celine Fasenmyer's doctoral work at the University of Michigan in 1945. Her technique, published as "Some Generalized Hypergeometric Polynomials" (Bulletin of the AMS, 1947), provided the first purely algorithmic method to find recurrence relations for sums of hypergeometric terms. Given a sum Σ_k F(n,k), her method assumes a recurrence exists, divides terms by F(n,k), simplifies factorial ratios, and solves the resulting linear system. Though computationally slower than later methods, her approach was the intellectual progenitor of all subsequent computerized techniques.

R. William Gosper's algorithm (1978) solved the indefinite hypergeometric summation problem with a landmark paper in PNAS: "Decision Procedure for Indefinite Hypergeometric Summation." Given a hypergeometric term a_n where a_{n+1}/a_n is rational, Gosper's algorithm determines whether a hypergeometric antidifference exists and computes it when possible. The algorithm's completeness—it never returns "unknown"—made it foundational for Zeilberger's later work. The key innovation involves the Gosper-Petkovšek representation, which factors the ratio r(n) into polynomials with specific coprimality conditions.

Doron Zeilberger revolutionized the field in 1990 with his creative telescoping algorithm, published in Discrete Mathematics ("A Fast Algorithm for Proving Terminating Hypergeometric Series Identities"). For definite sums, the algorithm finds a recurrence operator P and certificate G such that P(n)·F(n,k) = G(n,k+1) - G(n,k). Summing over k causes the right side to telescope, yielding a recurrence for the sum. The term "creative telescoping" was coined by Alf van der Poorten in his 1979 exposition of Apéry's irrationality proof for ζ(3).

The collaboration between Herbert Wilf and Doron Zeilberger produced the WZ method, described in their 1990 paper "Rational Functions Certify Combinatorial Identities" (Journal of the AMS). A WZ-pair (F,G) satisfies F(n+1,k) - F(n,k) = G(n,k+1) - G(n,k), where the rational function R(n,k) with G = R·F serves as a machine-verifiable proof certificate. Their 1992 paper in Inventiones Mathematicae extended the framework to multisum and integral identities. This work earned Wilf and Zeilberger the 1998 AMS Steele Prize for Seminal Contribution to Mathematics.

Marko Petkovšek's algorithm (1992) completed the picture by finding all hypergeometric solutions to linear recurrences with polynomial coefficients. Published in the Journal of Symbolic Computation, his "Hyper" algorithm determines whether Zeilberger's output recurrences have hypergeometric closed forms. Together, these five algorithms—Fasenmyer, Gosper, Zeilberger, WZ, and Hyper—form the core toolkit described in the definitive textbook "A=B" (Petkovšek, Wilf, and Zeilberger, 1996), freely available online.

Zeilberger's experimental mathematics philosophy shaped the field

Beyond algorithms, Zeilberger has championed a computational philosophy that challenges traditional mathematical practice. Through his "Dr. Z's Opinions" website at Rutgers, he argues that computer-assisted proofs are often more rigorous and certain than human-generated ones (Opinion 112), and advocates moving from the "Greek (Axiomatic, Deductive)" to the "Babylonian (Algorithmic, Inductive, Experimental)" approach (Opinion 174). His ultrafinitist views—believing actual infinity is meaningless—inform his pragmatic methodology.

Zeilberger's software contributions center on EKHAD, named after his co-author "Shalosh B. Ekhad" (his computer, from Hebrew for "three-one," referencing his AT&T 3B1). This Maple package implements creative telescoping and the WZ method, computing recurrence relations and proof certificates automatically. The name appears as co-author on dozens of papers since the late 1980s.

The experimental methodology follows a systematic loop: computers generate conjectures by computing sequence terms and fitting patterns, then prove their own conjectures via creative telescoping and initial condition verification. Famous results include the proof of the Alternating Sign Matrix Conjecture (1996, Electronic Journal of Combinatorics), an 84-page proof recruited ~100 volunteer checkers, and the q-TSPP conjecture proof (Koutschan, Kauers, Zeilberger, PNAS 2011), which resolved a 28-year-old problem and won the 2016 David P. Robbins Prize.

Computer algebra systems implement identity discovery at scale

Modern CAS embed these algorithms in accessible packages. Mathematica provides Sum (using Gosper's algorithm), FindSequenceFunction for pattern detection, and FullSimplify with ~400 rules for special functions. The HolonomicFunctions package by Christoph Koutschan (RISC Linz, first released 2009) offers powerful creative telescoping for multivariate holonomic functions, enabling the Gessel lattice path conjecture proof (PNAS 2009).

Maple's ecosystem includes SumTools[Hypergeometric][Zeilberger] for creative telescoping, the gfun package (Salvy and Zimmermann, ACM TOMS 1994) for generating function manipulation, and Mgfun (Frédéric Chyzak, INRIA, 2000) for multivariate holonomic functions using Gröbner basis generalizations. The gfun package's listtorec and guessgf functions power the OEIS Superseeker service.

FORM, developed by Jos Vermaseren at Nikhef since 1984, specializes in manipulating extremely large algebraic expressions for high-energy physics. Written in C and open-sourced in 2010 under GPL v3, FORM handles expressions limited only by disk space and supports pattern matching, noncommutative algebras, and Gröbner bases (v4.0, 2013). It's essential for higher-order QCD calculations.

The theory of holonomic functions (D-finite) underlies much of this work. These functions satisfy linear differential equations with polynomial coefficients and form a ring closed under addition, multiplication, and definite integration. Stanley's 1980 paper "Differentiably Finite Power Series" (European Journal of Combinatorics) established foundations, while packages like ore_algebra (Kauers, Jaroschek, Johansson for SageMath) and NumGfun (Marc Mezzarobba) provide modern implementations.

Machine learning approaches have transformed mathematical discovery

The Ramanujan Machine (Raayoni et al., Nature 2021) from Technion pioneered algorithmic discovery of continued fraction formulas for fundamental constants. Using Meet-in-the-Middle and Descent&Repel algorithms, the system discovered dozens of formulas for π, e, and Catalan's constant—including a continued fraction for Catalan's constant with record approximation efficiency. Several conjectures remain unproved, demonstrating the gap between empirical discovery and formal proof.

Google DeepMind has produced remarkable results across multiple projects. Their 2021 Nature paper "Advancing mathematics by guiding human intuition with AI" collaborated with Geordie Williamson (Sydney) and Oxford mathematicians to discover connections between knot invariants and geometry, leading to the concept of "natural slope." For representation theory, they made progress on the 40-year-old combinatorial invariance conjecture.

AlphaTensor (Nature 2022) reformulated algorithm discovery as a single-player game, using reinforcement learning to discover matrix multiplication algorithms faster than Strassen's 50-year-old method—47 steps vs. 49 for 4×4 matrices. The system found over 14,000 non-equivalent algorithms, some 10-20% faster on specific hardware.

FunSearch (Nature 2024) pairs large language models with evolutionary algorithms to search for functions written in code. This approach achieved the first LLM-based discovery for open mathematical problems, including the cap set problem and faster bin-packing algorithms. AlphaProof (Nature 2025) used AlphaZero-style reinforcement learning to achieve silver medal-level performance at the 2024 IMO, solving 3/5 non-geometry problems.

Facebook AI Research demonstrated sequence-to-sequence transformers for symbolic mathematics (Lample and Charton, ICLR 2020). Treating integration as language translation with prefix notation, their model achieved ~100% accuracy on function integration, outperforming Mathematica's ~85%. This work opened neural approaches to symbolic calculus.

Q-series and partition algorithms extend classical methods

The q-analogue of Zeilberger's algorithm (qZeil) by Peter Paule and Axel Riese (Fields Institute Communications, 1997) enables automatic proofs of q-hypergeometric summation identities. The RISC ErgoSum bundle at Johannes Kepler University provides comprehensive packages: qZeil for indefinite/definite summation, qMultiSum (Riese, J. Symbolic Computation 2003) for multiple summations, and Omega (Andrews, Paule, Riese) implementing MacMahon's Partition Analysis.

Peter Paule's 1994 paper "Short and Easy Computer Proofs of the Rogers-Ramanujan Identities" (Electronic Journal of Combinatorics) demonstrated that computers can produce elegant proofs with certificates in approximately 60 seconds. Computer searches in PARI/GP, Maple, and Mathematica continue discovering new Rogers-Ramanujan type identities.

For bijective proofs, the Involution Principle developed by Adriano Garsia and Stephen Milne (1981) produces bijections automatically for partition identities—their Rogers-Ramanujan bijection claimed George Andrews' $100 prize. The Snake Oil method, popularized in Wilf's "Generatingfunctionology" (1994), uses generating functions to discover (not just prove) combinatorial identities, handling cases beyond WZ's scope.

Integer sequences and automated conjecture systems drive discovery

Neil Sloane's OEIS represents the most successful mathematical database, growing from 2,372 sequences in his 1973 handbook to over 390,000 sequences with 12,000+ academic citations. The Superseeker service applies the gfun package and over 100 transformations to identify unknown sequences. Sloane's insight—that integer sequences serve as "fingerprints" connecting disparate mathematical domains—has facilitated countless discoveries.

GRAFFITI, developed by Siemion Fajtlowicz at the University of Houston (1988), pioneered automated conjecture generation in graph theory. Its Dalmatian heuristic filters trivial conjectures by requiring that accepted conjectures provide distinguishing examples extending current knowledge. Research on GRAFFITI conjectures produced over 60 publications and attracted attention from Paul Erdős and Ronald Graham. The successor TxGraffiti (Randy Davila, 2017) incorporates machine learning and linear optimization.

Simon Colton's HR system (PhD 2000, book 2002) performs automated theory formation by combining inductive concept formation with deductive verification using theorem provers (Otter) and model generators (MACE). HR discovered 20 new types of numbers accepted into OEIS, including refactorable numbers. The system operates across number theory, graph theory, and group theory.

AutoGraphiX (Caporossi and Hansen, GERAD Montreal, 2000) uses Variable Neighborhood Search to find extremal graphs, generating several hundred conjectures. Doug Lenat's AM (1976) and EURISKO (1976-1983) represented early AI approaches to mathematical discovery, though AM's claims of rediscovering Goldbach's conjecture faced later criticism. EURISKO's self-modifying heuristics won the US Traveller TCS tournament twice before frustrations with domain-specific knowledge led Lenat to create Cyc.

Algebraic simplification faces fundamental undecidability limits

Richardson's theorem (1968) establishes that for expressions involving integers, π, ln(2), exponentials, sine, and absolute value, determining zero-equivalence is undecidable—proven via reduction from Hilbert's Tenth Problem. This fundamental barrier means no algorithm can reliably simplify arbitrary transcendental expressions.

For polynomials, Gröbner bases provide a decision procedure. Bruno Buchberger's 1965 PhD thesis introduced the algorithm that transforms polynomial sets into canonical forms where ideal membership becomes division remainder checking. The F4/F5 algorithms by Faugère dramatically improved efficiency. Applications include identity verification in polynomial rings, though worst-case complexity is doubly exponential.

The Knuth-Bendix completion algorithm (1970) transforms equations into confluent, terminating rewriting systems. When completion succeeds, two terms are equivalent if and only if they reduce to the same normal form. This provides a general framework for equational reasoning, with Buchberger's algorithm being its instantiation for polynomial ideals.

For nested radicals, Susan Landau's 1989 algorithm (SIAM J. Computing) provides the first complete procedure for deciding denestability and computing denestings. The Risch algorithm (1969-1970) decides whether elementary functions have elementary antiderivatives, with Manuel Bronstein's 1997 book providing the definitive modern treatment. Identity discovery emerges when the algorithm determines expressions must simplify in specific ways.

Historical timeline reveals accelerating progress

| Period | Milestone | Contributors | |--------|-----------|--------------| | 1945-1949 | Sister Celine's technique | Mary Celine Fasenmyer | | 1965 | Gröbner bases | Bruno Buchberger | | 1968 | Undecidability of zero-equivalence | Daniel Richardson | | 1970 | Knuth-Bendix completion | Donald Knuth, Peter Bendix | | 1976 | AM automated mathematician | Douglas Lenat | | 1978 | Gosper's algorithm | R. William Gosper | | 1988 | GRAFFITI conjecture system | Siemion Fajtlowicz | | 1990 | Creative telescoping, WZ method | Zeilberger, Wilf | | 1992 | Petkovšek's algorithm | Marko Petkovšek | | 1994 | OEIS online | Neil Sloane | | 1996 | "A=B" published | Petkovšek, Wilf, Zeilberger | | 2002 | HR automated theory formation | Simon Colton | | 2020 | Neural symbolic integration | Facebook AI Research | | 2021 | Ramanujan Machine | Technion | | 2022 | AlphaTensor | Google DeepMind | | 2024 | FunSearch | Google DeepMind |

Software implementations enable practical application

The field offers rich software ecosystems. Maple packages include EKHAD and qEKHAD (Zeilberger), gfun/Mgfun (Salvy, Zimmermann, Chyzak), and SumTools built into the core system. Mathematica packages include HolonomicFunctions (Koutschan), fastZeil (Paule/Schorn), and built-in hypergeometric simplification. SageMath provides ore_algebra, NumGfun, and interfaces to underlying systems.

The RISC ErgoSum bundle (risc.jku.at/research/combinat/software) offers comprehensive combinatorics tools: qZeil, qMultiSum, MultiSum, Omega, HolonomicFunctions, and the Guess package for sequence fitting. SymPy provides gosper_sum and hypergeometric tools, while REDUCE offers the ZEILBERG package (Koepf and Stölting).

For automated conjecture, TxGraffiti is available as an interactive website, and the Ramanujan Machine code is open-source at ramanujanmachine.com. DeepMind's work remains largely proprietary, though some implementations appear in subsequent academic reproductions.

Conclusion: convergence of symbolic and neural methods

The trajectory from Sister Celine's hand calculations to AlphaProof's IMO-level theorem proving reveals a fundamental shift in mathematical practice. Classical algorithms like Gosper's and Zeilberger's provided completeness guarantees—they always succeed or definitively fail—while modern neural approaches trade guarantees for broader applicability and creative exploration.

The most powerful current systems combine both paradigms: FunSearch uses LLMs for creative generation with evolutionary algorithms for verification; AlphaProof pairs neural networks with formal verification in Lean. This hybrid approach—neural intuition guided by symbolic verification—may represent the future of mathematical discovery, enabling exploration of spaces too vast for exhaustive search while maintaining the rigor that distinguishes mathematics from conjecture.

What remains remarkable is how much human mathematicians accomplished without these tools. Ramanujan discovered continued fractions by hand that modern algorithms still struggle to prove. Yet the field has progressed from proving known identities to discovering new ones, from verifying conjectures to generating them. The automation of mathematical discovery, once considered impossible, has become reality—though the deepest mysteries, as Richardson's theorem reminds us, remain forever beyond any algorithm's reach.