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

DOI10.1007/S10817-015-9338-0zbMATH Open1356.68190OpenAlexW1755672467WikidataQ113901250 ScholiaQ113901250MaRDI QIDQ286798FDOQ286798

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

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

zbMATH Keywords

formal proofhypergeometric summation

Mathematics Subject Classification ID

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

Cites Work

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

Cited In (5)

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

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)