Skip to main content

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_toappear,
    publisher        = {Springer},
    author           = {Chan, Hing-Lun and Norrish, Michael},
    year             = {To appear},
    keywords         = {least common multiple; pascal’s triangle; leibniz’s triangle; formalisation; automated theorem
                        proving; hol4; binomial coefficients},
    title            = {Proof Pearl: Bounding Least Common Multiples with Triangles},
    journal          = {Journal of Automated Reasoning}
  }

Download

Served by Apache on Linux on seL4.