Q5856420 (Q5856420): Difference between revisions

@@ Property / describes a project that uses @@
+Coq-Combi
@@ Property / describes a project that uses: Coq-Combi / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Lean
@@ Property / describes a project that uses: Lean / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Coq
@@ Property / describes a project that uses: Coq / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Isabelle/HOL
@@ Property / describes a project that uses: Isabelle/HOL / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Algolib
@@ Property / describes a project that uses: Algolib / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+CakeML
@@ Property / describes a project that uses: CakeML / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Archive Formal Proofs
@@ Property / describes a project that uses: Archive Formal Proofs / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Mathematical Components
@@ Property / describes a project that uses: Mathematical Components / rank @@
+Normal rank
@@ Property / MaRDI profile type @@
+MaRDI publication profile
@@ Property / MaRDI profile type: MaRDI publication profile / rank @@
+Normal rank
@@ Property / cites work @@
+Q5195290
@@ Property / cites work: Q5195290 / rank @@
+Normal rank
@@ Property / cites work @@
+A formally verified proof of the prime number theorem
+Normal rank
@@ Property / cites work @@
+Q4101884
@@ Property / cites work: Q4101884 / rank @@
+Normal rank
@@ Property / cites work @@
+Setoids in type theory
@@ Property / cites work: Setoids in type theory / rank @@
+Normal rank
@@ Property / cites work @@
+Fast Reflexive Arithmetic Tactics the Linear Case and Beyond
+Normal rank
@@ Property / cites work @@
+A Note on the Irrationality of ζ(2) and ζ(3)
@@ Property / cites work: A Note on the Irrationality of ζ(2) and ζ(3) / rank @@
+Normal rank
@@ Property / cites work @@
+Q5195244
@@ Property / cites work: Q5195244 / rank @@
+Normal rank
@@ Property / cites work @@
+Irrationality of infinitely many values of the zeta function at odd integers.
+Normal rank
@@ Property / cites work @@
+A Computer-Algebra-Based Formal Proof of the Irrationality of ζ(3)
+Normal rank
@@ Property / cites work @@
+Construction of Real Algebraic Numbers in Coq
@@ Property / cites work: Construction of Real Algebraic Numbers in Coq / rank @@
+Normal rank
@@ Property / cites work @@
+Dealing with algebraic expressions over a field in Coq using Maple
+Normal rank
@@ Property / cites work @@
+Verified Real Asymptotics in Isabelle/HOL
@@ Property / cites work: Verified Real Asymptotics in Isabelle/HOL / rank @@
+Normal rank
@@ Property / cites work @@
+A simple elementary proof for the inequality \(d_n< 3^n\)
+Normal rank
@@ Property / cites work @@
+Q4831115
@@ Property / cites work: Q4831115 / rank @@
+Normal rank
@@ Property / cites work @@
+Many odd zeta values are irrational
@@ Property / cites work: Many odd zeta values are irrational / rank @@
+Normal rank
@@ Property / cites work @@
+Packaging Mathematical Structures
@@ Property / cites work: Packaging Mathematical Structures / rank @@
+Normal rank
@@ Property / cites work @@
+A compiled implementation of strong reduction
@@ Property / cites work: A compiled implementation of strong reduction / rank @@
+Normal rank
@@ Property / cites work @@
+Theorem Proving in Higher Order Logics
@@ Property / cites work: Theorem Proving in Higher Order Logics / rank @@
+Normal rank
@@ Property / cites work @@
+A Computational Approach to Pocklington Certificates in Type Theory
+Normal rank
@@ Property / cites work @@
+On the Product of the Primes
@@ Property / cites work: On the Product of the Primes / rank @@
+Normal rank
@@ Property / cites work @@
+Formalizing an analytic proof of the prime number theorem
+Normal rank
@@ Property / cites work @@
+Formal proofs of hypergeometric sums. Dedicated to the memory of Andrzej Trybulec
+Normal rank
@@ Property / cites work @@
+A coherence theorem for Martin-Löf's type theory
@@ Property / cites work: A coherence theorem for Martin-Löf's type theory / rank @@
+Normal rank
@@ Property / cites work @@
+A verified compiler from Isabelle/HOL to CakeML
@@ Property / cites work: A verified compiler from Isabelle/HOL to CakeML / rank @@
+Normal rank
@@ Property / cites work @@
+A Skeptic's approach to combining HOL and Maple
@@ Property / cites work: A Skeptic's approach to combining HOL and Maple / rank @@
+Normal rank
@@ Property / cites work @@
+Q4649560
@@ Property / cites work: Q4649560 / rank @@
+Normal rank
@@ Property / cites work @@
+Canonical Structures for the Working Coq User
@@ Property / cites work: Canonical Structures for the Working Coq User / rank @@
+Normal rank
@@ Property / cites work @@
+La fonction zêta de Riemann prend une infinité de valeurs irrationnelles aux entiers impairs
+Normal rank
@@ Property / cites work @@
+Q3075239
@@ Property / cites work: Q3075239 / rank @@
+Normal rank
@@ Property / cites work @@
+A proof that Euler missed. Apéry's proof of the irrationality of \(\zeta(3)\). An informal report
+Normal rank
@@ Property / cites work @@
+The meaning of infinity in calculus and computer algebra systems
+Normal rank
@@ Property / cites work @@
+A holonomic systems approach to special functions identities
+Normal rank
@@ Property / cites work @@
+The method of creative telescoping
@@ Property / cites work: The method of creative telescoping / rank @@
+Normal rank
@@ links / mardi / name / links / mardi / name @@
+Publication:5856420