scientific article; zbMATH DE number 7327949

MaRDI QIDQ5856420

Assia Mahboubi, Thomas Sibut-Pinote

Publication date: 26 March 2021

Full work available at URL: https://arxiv.org/abs/1912.06611

Title: zbMATH Open Web Interface contents unavailable due to conflicting licenses.

zbMATH Keywords

Riemann zeta functionsymbolic computationirrationalitynumber theoryformal proofCoqcreative telescopingApéry's recurrences

Mathematics Subject Classification ID

Logic in computer science (03B70) Computer science (68-XX)

Related Items

A bi-directional extensible interface between Lean and Mathematica ⋮ Mathematics and the formal turn

Uses Software

• Coq
• Maple
• Isabelle/HOL
• CoqEAL
• Algolib
• HOL Light
• CakeML
• Lean
• Archive Formal Proofs
• Mathematical Components
• Coq-Combi
• Zeta_3_Irrational

Cites Work

• Formal proofs of hypergeometric sums. Dedicated to the memory of Andrzej Trybulec
• A holonomic systems approach to special functions identities
• The method of creative telescoping
• 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
• A verified compiler from Isabelle/HOL to CakeML
• The meaning of infinity in calculus and computer algebra systems
• Dealing with algebraic expressions over a field in Coq using Maple
• A simple elementary proof for the inequality \(d_n< 3^n\)
• Formalizing an analytic proof of the prime number theorem
• A Computer-Algebra-Based Formal Proof of the Irrationality of ζ(3)
• Construction of Real Algebraic Numbers in Coq
• A compiled implementation of strong reduction
• Packaging Mathematical Structures
• A Computational Approach to Pocklington Certificates in Type Theory
• Fast Reflexive Arithmetic Tactics the Linear Case and Beyond
• A Note on the Irrationality of ζ(2) and ζ(3)
• A coherence theorem for Martin-Löf's type theory
• Setoids in type theory
• La fonction zêta de Riemann prend une infinité de valeurs irrationnelles aux entiers impairs
• Verified Real Asymptotics in Isabelle/HOL
• A formally verified proof of the prime number theorem
• Canonical Structures for the Working Coq User
• Many odd zeta values are irrational
• Theorem Proving in Higher Order Logics
• On the Product of the Primes
• Irrationality of infinitely many values of the zeta function at odd integers.
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: