Formal proofs of hypergeometric sums. Dedicated to the memory of Andrzej Trybulec

DOI10.1007/S10817-015-9338-0MaRDI QIDQ286798zbMATH OpenOpenAlexWikidataFDO

Authors John Harrison

Publication date 26 May 2016

Published in Journal of Automated Reasoning (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/s10817-015-9338-0

zbMATH Keywords

formal proofhypergeometric summation

Mathematics Subject Classification ID

Symbolic computation of special functions (Gosper and Zeilberger algorithms, etc.) (33F10)

Recommendations

• What is \dots a Wilf-Zeilberger pair?
• scientific article; zbMATH DE number 434742
• An algorithmic proof theory for hypergeometric (ordinary and ``\(q\)) multisum/integral identities
• Towards computerized proofs of identities
• The proof of the WZ method for some hypergeometric-type series identities

Cites work

• scientific article; zbMATH DE number 3621859 (Why is no real title available?)
• scientific article; zbMATH DE number 1268810 (Why is no real title available?)
• scientific article; zbMATH DE number 3232102 (Why is no real title available?)
• A Computational Approach to Pocklington Certificates in Type Theory
• A Computer-Algebra-Based Formal Proof of the Irrationality of ζ(3)
• A Note on the Irrationality of ζ(2) and ζ(3)
• A Skeptic's approach to combining HOL and Maple
• A holonomic systems approach to special functions identities
• A proof that Euler missed. Apéry's proof of the irrationality of \(\zeta(3)\). An informal report
• Apéry's double sum is plain sailing indeed
• Complex Analysis
• Decision procedure for indefinite hypergeometric summation
• Finding identities with the WZ method
• Formal and efficient primality proofs by use of computer algebra oracles
• How To Do Monthly Problems With Your Computer
• Number Theory
• On the formalization of gamma function in HOL
• Primality Proving with Elliptic Curves
• Rational Functions Certify Combinatorial Identities
• The Binomial Coefficient Function

Cited in

(5)

• Proof of the Wilf-Zeilberger conjecture for mixed hypergeometric terms
• Some open problems related to creative telescoping
• Verified interactive computation of definite integrals
• A formal proof of the irrationality of \(\zeta(3)\)
• A bi-directional extensible interface between Lean and Mathematica

Describes a project that uses

Uses Software

• HOL Light

This page was built for publication: Formal proofs of hypergeometric sums. Dedicated to the memory of Andrzej Trybulec

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q286798)