DATA61
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.
@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} }