Proof pearl: Bounding least common multiples with triangles
type: Item
instance of: scholarly article
title: Proof pearl: Bounding least common multiples with triangles
zbMATH Open document ID: 1468.68284
author: Hing-Lun Chan
author: Michael Norrish
published in: Journal of Automated Reasoning
publication date: 2019-02-18T00:00:00Z
Mathematics Subject Classification ID: 68V15
Mathematics Subject Classification ID: 11A05
Mathematics Subject Classification ID: 68V20
zbMATH DE Number: 7024455
zbMATH Keywords: least common multiple
zbMATH Keywords: Pascal's triangle
zbMATH Keywords: Leibniz's triangle
zbMATH Keywords: formalisation
zbMATH Keywords: automated theorem proving
zbMATH Keywords: HOL4
zbMATH Keywords: binomial coefficients
describes a project that uses: HOL
MaRDI profile type: Publication
full work available at URL: s10817-017-9438-0
OpenAlex ID: W2762997874
cites work: PRIMES is in P
cites work: About the Formalization of Some Results by Chebyshev in Number Theory
cites work: A formally verified proof of the prime number theorem
cites work: The Harmonic Triangle and the Beta Function
cites work: Q3932807
cites work: Mechanisation of AKS Algorithm: Part 1 – The Main Theorem
cites work: Proof Pearl: Bounding Least Common Multiples with Triangles
cites work: A Computer-Algebra-Based Formal Proof of the Irrationality of ζ(3)
cites work: Q4781157
cites work: Euler's beta integral in Pietro Mengoli's works
cites work: An Identity Involving the Least Common Multiple of Binomial Coefficients and Its Application
cites work: An epic drama: the development of the prime number theorem
cites work: On the Product of the Primes
cites work: Q3518705
cites work: Formalizing an analytic proof of the prime number theorem
cites work: On Chebyshev-Type Inequalities for Primes
DOI: 10.1007/S10817-017-9438-0
description: scientific article; zbMATH DE number 7024455