Skip to main content

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

    publisher        = {Springer},
    doi              = {10.1007/s10817-017-9438-0},
    issue            = {2},
    journal          = {Journal of Automated Reasoning},
    author           = {Chan, Hing-Lun and Norrish, Michael},
    month            = feb,
    volume           = {62},
    keywords         = {least common multiple; pascal’s triangle; leibniz’s triangle; formalisation; automated theorem
                        proving; hol4; binomial coefficients},
    year             = {2019},
    date             = {2019-2-10},
    title            = {Proof Pearl: Bounding Least Common Multiples with Triangles},
    pages            = {171-192}


Served by Apache on Linux on seL4.