Proof pearl: Bounding least common multiples with triangles
DOI10.1007/S10817-017-9438-0zbMATH Open1468.68284OpenAlexW2762997874MaRDI QIDQ1722641FDOQ1722641
Authors: Hing-Lun Chan, Michael Norrish 
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
Recommendations
binomial coefficientsautomated theorem provingPascal's triangleformalisationHOL4least common multipleLeibniz's triangle
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)
Cites Work
- An introduction to the theory of numbers. Edited and revised by D. R. Heath-Brown and J. H. Silverman. With a foreword by Andrew Wiles
- PRIMES is in P
- A Computer-Algebra-Based Formal Proof of the Irrationality of ζ(3)
- A formally verified proof of the prime number theorem
- The Harmonic Triangle and the Beta Function
- On Chebyshev-Type Inequalities for Primes
- On the Product of the Primes
- Title not available (Why is that?)
- An Identity Involving the Least Common Multiple of Binomial Coefficients and Its Application
- Euler's beta integral in Pietro Mengoli's works
- About the Formalization of Some Results by Chebyshev in Number Theory
- Formalizing an analytic proof of the prime number theorem
- Proof pearl: Bounding least common multiples with triangles
- An epic drama: the development of the prime number theorem
- Mechanisation of AKS algorithm. I. The main theorem
- Title not available (Why is that?)
Cited In (3)
Uses Software
This page was built for publication: Proof pearl: Bounding least common multiples with triangles
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1722641)
