Proof Pearl: Bounding Least Common Multiples with Triangles
Date
2017
Authors
Chan, Hing Lun Joseph
Norrish, Michael
Journal Title
Journal ISSN
Volume Title
Publisher
Kluwer Academic Publishers
Abstract
We present a proof of the fact that Open image in new window for \(n \ge 0\). This result has a standard proof via an integral, but our proof is purely number-theoretic, requiring little more than inductions based on lists. The almost-pictorial proof is based on manipulations of a variant of Leibniz’s harmonic triangle, itself a relative of Pascal’s better-known Triangle.
Description
Keywords
Least common multiple, Pascal’s triangle, Leibniz’s triangle, Formalisation, Automated theorem proving, HOL4, Binomial coefficients
Citation
Collections
Source
Journal of Automated Reasoning
Type
Journal article
Book Title
Entity type
Access Statement
License Rights
Restricted until
2099-12-31
Downloads
File
Description