Skip to main content
CSIRO Logo Data 61 logo

Proof pearl: Bounding least common multiples with triangles

Authors

Joseph Chan and Michael Norrish

Australian National University

Data61
CSIRO

Abstract

We present a proof of the fact that 2^n ≤ lcm{1 . . . (n + 1)}. This result has a standard proof via an integral, but our proof is purely number theoretic, requiring little more than list inductions. The proof is based on manipulations of a variant of Leibniz’s Harmonic Triangle, itself a relative of Pascal’s better-known Triangle.

BibTeX Entry

  @inproceedings{Chan_Norrish_16,
    author           = {Chan, Joseph and Norrish, Michael},
    editor           = {{Jasmin Christian Blanchette and Stephan Merz}},
    month            = aug,
    year             = {2016},
    title            = {Proof Pearl: Bounding Least Common Multiples with Triangles},
    address          = {Nancy, France},
    pages            = {140--150},
    booktitle        = {International Conference on Interactive Theorem Proving},
    paperurl         = {https://ts.data61.csiro.au/publications/nicta_full_text/9267.pdf},
    publisher        = {Springer},
    slides           = {/publications/nicta_slides/9267.pdf},
    isbn             = {9783319431437}
  }

Download