Proof pearl: Bounding least common multiples with triangles

DOI10.1007/s10817-017-9438-0zbMath1468.68284OpenAlexW2762997874MaRDI QIDQ1722641

Michael Norrish, Hing-Lun Chan

Publication date: 18 February 2019

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

Full work available at URL: https://doi.org/10.1007/s10817-017-9438-0

zbMATH Keywords

least common multiplebinomial coefficientsautomated theorem provingPascal's triangleformalisationHOL4Leibniz's triangle

Mathematics Subject Classification ID

Multiplicative structure; Euclidean algorithm; greatest common divisors (11A05) Formalization of mathematics in connection with theorem provers (68V20) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Related Items (1)

Mechanisation of the AKS algorithm

Uses Software

• HOL

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Euler's beta integral in Pietro Mengoli's works
• PRIMES is in P
• Formalizing an analytic proof of the prime number theorem
• Proof Pearl: Bounding Least Common Multiples with Triangles
• A Computer-Algebra-Based Formal Proof of the Irrationality of ζ(3)
• Mechanisation of AKS Algorithm: Part 1 – The Main Theorem
• The Harmonic Triangle and the Beta Function
• An Identity Involving the Least Common Multiple of Binomial Coefficients and Its Application
• About the Formalization of Some Results by Chebyshev in Number Theory
• On Chebyshev-Type Inequalities for Primes
• A formally verified proof of the prime number theorem
• On the Product of the Primes

This page was built for publication: Proof pearl: Bounding least common multiples with triangles