Proof Pearl: Bounding Least Common Multiples with Triangles

Hing Lun Chan; Michael Norrish

doi:10.1007/s10817-017-9438-0

Proof Pearl: Bounding Least Common Multiples with Triangles

Hing Lun Chan^*
, Michael Norrish

^*Corresponding author for this work

Research output: Contribution to journal › Article › peer-review

2 Citations (Scopus)

Abstract

We present a proof of the fact that [InlineEquation not available: see fulltext.] 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.

Original language	English
Pages (from-to)	171-192
Number of pages	22
Journal	Journal of Automated Reasoning
Volume	62
Issue number	2
DOIs	https://doi.org/10.1007/s10817-017-9438-0
Publication status	Published - 15 Feb 2019

Access to Document

10.1007/s10817-017-9438-0

Cite this

@article{4cb96e3dc3c54eafbe0448401a09cd4b,

title = "Proof Pearl: Bounding Least Common Multiples with Triangles",

abstract = "We present a proof of the fact that [InlineEquation not available: see fulltext.] 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{\textquoteright}s harmonic triangle, itself a relative of Pascal{\textquoteright}s better-known Triangle.",

keywords = "Automated theorem proving, Binomial coefficients, Formalisation, HOL4, Least common multiple, Leibniz{\textquoteright}s triangle, Pascal{\textquoteright}s triangle",

author = "Chan, \{Hing Lun\} and Michael Norrish",

note = "Publisher Copyright: {\textcopyright} 2017, Springer Science+Business Media B.V.",

year = "2019",

month = feb,

day = "15",

doi = "10.1007/s10817-017-9438-0",

language = "English",

volume = "62",

pages = "171--192",

journal = "Journal of Automated Reasoning",

issn = "0168-7433",

publisher = "Springer Netherlands",

number = "2",

}

TY - JOUR

T1 - Proof Pearl

T2 - Bounding Least Common Multiples with Triangles

AU - Chan, Hing Lun

AU - Norrish, Michael

PY - 2019/2/15

Y1 - 2019/2/15

N2 - We present a proof of the fact that [InlineEquation not available: see fulltext.] 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.

AB - We present a proof of the fact that [InlineEquation not available: see fulltext.] 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.

KW - Automated theorem proving

KW - Binomial coefficients

KW - Formalisation

KW - HOL4

KW - Least common multiple

KW - Leibniz’s triangle

KW - Pascal’s triangle

UR - https://www.scopus.com/pages/publications/85031406482

U2 - 10.1007/s10817-017-9438-0

DO - 10.1007/s10817-017-9438-0

M3 - Article

SN - 0168-7433

VL - 62

SP - 171

EP - 192

JO - Journal of Automated Reasoning

JF - Journal of Automated Reasoning

IS - 2

ER -

Proof Pearl: Bounding Least Common Multiples with Triangles

Abstract

Access to Document

Other files and links

Fingerprint

Cite this