Trustworthy Systems

Proof pearl: Bounding least common multiples with triangles


Hing-Lun Chan and Michael Norrish


Australian National University


We present a proof of the fact that 2^n ≤ LCM{1,2,3,...,(n + 1)} ≤ 4^(n + 1) for n ≥ 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.

BibTeX Entry

    author           = {Chan, Hing-Lun and Norrish, Michael},
    date             = {2019-2-10},
    doi              = {},
    issue            = {2},
    journal          = {Journal of Automated Reasoning},
    keywords         = {Least common multiple; Pascal’s triangle; Leibniz’s triangle; Formalisation; Automated theorem
                        proving; {HOL4}; Binomial coefficients},
    month            = feb,
    pages            = {171-192},
    paperurl         = {},
    publisher        = {Springer},
    title            = {Proof Pearl: Bounding Least Common Multiples with Triangles},
    volume           = {62},
    year             = {2019}