Trustworthy Systems

Proof pearl: Bounding least common multiples with triangles

Authors

Hing-Lun Chan and Michael Norrish

DATA61

Australian National University

Abstract

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

  @article{Chan_Norrish_19,
    doi              = {https://doi.org/10.1007/s10817-017-9438-0},
    publisher        = {Springer},
    month            = feb,
    journal          = {Journal of Automated Reasoning},
    paperurl         = {https://trustworthy.systems/publications/csiro_full_text/Chan_Norrish_19.pdf},
    year             = {2019},
    issue            = {2},
    keywords         = {Least common multiple; Pascal’s triangle; Leibniz’s triangle; Formalisation; Automated theorem
                        proving; {HOL4}; Binomial coefficients},
    volume           = {62},
    title            = {Proof Pearl: Bounding Least Common Multiples with Triangles},
    pages            = {171-192},
    author           = {Chan, Hing-Lun and Norrish, Michael},
    date             = {2019-2-10}
  }

Download