Journal of Automated Reasoning

, Volume 62, Issue 2, pp 171–192 | Cite as

Proof Pearl: Bounding Least Common Multiples with Triangles

  • Hing-Lun ChanEmail author
  • Michael Norrish


We present a proof of the fact that Open image in new window for \(n \ge 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.


Least common multiple Pascal’s triangle Leibniz’s triangle Formalisation Automated theorem proving HOL4 Binomial coefficients 


  1. 1.
    Agrawal, M., Kayal, N., Saxena, N.: PRIMES is in P. Ann. Math. 160(2), 781–793 (2004)MathSciNetCrossRefzbMATHGoogle Scholar
  2. 2.
    Asperti, A., Ricciotti, W.: About the formalization of some results by Chebyshev in number theory. In: Types for Proofs and Programs, International Conference, TYPES 2008, Torino, Italy, March 26–29, 2008, Revised Selected Papers, pp. 19–31 (2008)Google Scholar
  3. 3.
    Avigad, J., Donnelly, K., Gray, D., Raff, P.: A formally verified proof of the prime number theorem. ACM Trans. Comput. Logic 9(1), 2 (2007). doi: 10.1145/1297658.1297660 MathSciNetCrossRefzbMATHGoogle Scholar
  4. 4.
    Ayoub, A.B.: The harmonic triangle and the beta function. Math. Mag. 60(4), 223–225 (1987)MathSciNetCrossRefzbMATHGoogle Scholar
  5. 5.
    Bicknell-Johnson, M.: Diagonal sums in the harmonic triangle. Fibonacci Quart. 19(3), 196–199 (1981)MathSciNetzbMATHGoogle Scholar
  6. 6.
    Chan, H.-L., Norrish, M.: Mechanisation of AKS Algorithm: Part 1–the main theorem. In: Urban, C., Zhang, X. (eds.) Interactive Theorem Proving, ITP 2015, Number 9236 in LNCS, pp. 117–136. Springer, Berlin (2015)Google Scholar
  7. 7.
    Chan, H.-L., Norrish, M.: Proof pearl: bounding least common multiples with triangles. In: Blanchette, J.C., Merz, S. (eds.) Interactive Theorem Proving, ITP 2016, Number 9807 in LNCS, pp. 140–150. Springer, Berlin (2016)Google Scholar
  8. 8.
    Chyzak, F., Mahboubi, A., Sibut-Pinote, T., Tassi, E.: A computer-algebra-based formal proof of the irrationality of \(\zeta \)(3). In: Klein, G., Gamboa, R. (eds) Interactive Theorem Proving: 5th International Conference, ITP 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 14–17, 2014. Proceedings, pp. 160–176. Springer, Cham (2014)Google Scholar
  9. 9.
    Edwards, A.W.F.: Pascal’s Arithmetical Triangle: The Story of a Mathematical Idea. Johns Hopkins University Press, Baltimore (2002)zbMATHGoogle Scholar
  10. 10.
    Esteve, M.R.M., Delshams, A.: Euler’s beta function in Pietro Mengoli’s works. Arch. Hist. Exact Sci. 63(3), 325–356 (2009)MathSciNetCrossRefzbMATHGoogle Scholar
  11. 11.
    Farhi, B.: An identity involving the least common multiple of binomial coefficients and its application. Am. Math. Month. 116(9), 836–839 (2009)MathSciNetCrossRefzbMATHGoogle Scholar
  12. 12.
    Fine, B., Rosenberger, G.: An epic drama: the development of the prime number theorem. Sci. Ser. A Math. Sci. 20:1–26 (2010).
  13. 13.
    Hanson, D.: On the product of the primes. Can. Math. Bull. 15(1), 33–37 (1972)CrossRefzbMATHGoogle Scholar
  14. 14.
    Hardy, G.H., Wright, E.M.: An Introduction to the Theory of Numbers, 6th edn. Oxford University Press, Oxford (2008). ISBN: 9780199219865zbMATHGoogle Scholar
  15. 15.
    Harrison, J.: Formalizing an analytic proof of the Prime Number Theorem (dedicated to Mike Gordon on the occasion of his 60th birthday). J. Autom. Reason. 43, 243–261 (2009)CrossRefGoogle Scholar
  16. 16.
    Hong, S., Nair’s, F.: Identities involving the least common multiple of binomial coefficients are equivalent (2009).
  17. 17.
    Grigory, M.: Answer to: Is there a Direct Proof of this LCM identity?. Question 1442 on Math Stack Exchange (2010).
  18. 18.
    Nair, M.: On Chebyshev-type inequalities for primes. Am. Math. Month. 89(2), 126–129 (1982)MathSciNetCrossRefzbMATHGoogle Scholar
  19. 19.
    Nicolas, A.: Answer to: Reason for LCM of all numbers from \(1 .. n\) equals roughly \(e^n\)?. Question 1111334 on Math Stack Exchange (2015).
  20. 20.
    Tao, T.: Structure and randomness in the prime numbers. A talk delivered at the Science colloquium (2007).

Copyright information

© Springer Science+Business Media B.V. 2017

Authors and Affiliations

  1. 1.Data61CSIROCanberraAustralia
  2. 2.Australian National UniversityCanberraAustralia

Personalised recommendations