Proof pearl: Bounding least common multiples with triangles

Hing Lun Chan; Michael Norrish

doi:10.1007/978-3-319-43144-4_9

Proof pearl: Bounding least common multiples with triangles

Hing Lun Chan^*, Michael Norrish

^*Corresponding author for this work

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

3 Citations (Scopus)

Abstract

We present a proof of the fact that 2ⁿ ≤ lcm{1, 2, 3, …, (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.

Original language	English
Title of host publication	Interactive Theorem Proving - 7th International Conference, ITP 2016, Proceedings
Editors	Jasmin Christian Blanchette, Stephan Merz
Publisher	Springer Verlag
Pages	140-150
Number of pages	11
ISBN (Print)	9783319431437
DOIs	https://doi.org/10.1007/978-3-319-43144-4_9
Publication status	Published - 2016
Event	7th International Conference on Interactive Theorem Proving, ITP 2016 - Nancy, France Duration: 22 Aug 2016 → 25 Aug 2016

Publication series

Name	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume	9807 LNCS
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Conference

Conference	7th International Conference on Interactive Theorem Proving, ITP 2016
Country/Territory	France
City	Nancy
Period	22/08/16 → 25/08/16

Access to Document

10.1007/978-3-319-43144-4_9

Cite this

Chan, H. L., & Norrish, M. (2016). Proof pearl: Bounding least common multiples with triangles. In J. C. Blanchette, & S. Merz (Eds.), Interactive Theorem Proving - 7th International Conference, ITP 2016, Proceedings (pp. 140-150). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 9807 LNCS). Springer Verlag. https://doi.org/10.1007/978-3-319-43144-4_9

Chan, Hing Lun ; Norrish, Michael. / Proof pearl : Bounding least common multiples with triangles. Interactive Theorem Proving - 7th International Conference, ITP 2016, Proceedings. editor / Jasmin Christian Blanchette ; Stephan Merz. Springer Verlag, 2016. pp. 140-150 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).

@inproceedings{d6d82bb45f504614b9ca5addb7fbf74a,

title = "Proof pearl: Bounding least common multiples with triangles",

abstract = "We present a proof of the fact that 2n ≤ lcm{1, 2, 3, …, (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{\textquoteright}s Harmonic Triangle, itself a relative of Pascal{\textquoteright}s better-known Triangle.",

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

note = "Publisher Copyright: {\textcopyright} Springer International Publishing Switzerland 2016.; 7th International Conference on Interactive Theorem Proving, ITP 2016 ; Conference date: 22-08-2016 Through 25-08-2016",

year = "2016",

doi = "10.1007/978-3-319-43144-4_9",

language = "English",

isbn = "9783319431437",

series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

publisher = "Springer Verlag",

pages = "140--150",

editor = "Blanchette, {Jasmin Christian} and Stephan Merz",

booktitle = "Interactive Theorem Proving - 7th International Conference, ITP 2016, Proceedings",

address = "Germany",

}

Chan, HL & Norrish, M 2016, Proof pearl: Bounding least common multiples with triangles. in JC Blanchette & S Merz (eds), Interactive Theorem Proving - 7th International Conference, ITP 2016, Proceedings. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 9807 LNCS, Springer Verlag, pp. 140-150, 7th International Conference on Interactive Theorem Proving, ITP 2016, Nancy, France, 22/08/16. https://doi.org/10.1007/978-3-319-43144-4_9

Proof pearl: Bounding least common multiples with triangles. / Chan, Hing Lun; Norrish, Michael.
Interactive Theorem Proving - 7th International Conference, ITP 2016, Proceedings. ed. / Jasmin Christian Blanchette; Stephan Merz. Springer Verlag, 2016. p. 140-150 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 9807 LNCS).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

TY - GEN

T1 - Proof pearl

T2 - 7th International Conference on Interactive Theorem Proving, ITP 2016

AU - Chan, Hing Lun

AU - Norrish, Michael

PY - 2016

Y1 - 2016

N2 - We present a proof of the fact that 2n ≤ lcm{1, 2, 3, …, (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.

AB - We present a proof of the fact that 2n ≤ lcm{1, 2, 3, …, (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.

UR - http://www.scopus.com/inward/record.url?scp=84984791890&partnerID=8YFLogxK

U2 - 10.1007/978-3-319-43144-4_9

DO - 10.1007/978-3-319-43144-4_9

M3 - Conference contribution

SN - 9783319431437

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 140

EP - 150

BT - Interactive Theorem Proving - 7th International Conference, ITP 2016, Proceedings

A2 - Blanchette, Jasmin Christian

A2 - Merz, Stephan

PB - Springer Verlag

Y2 - 22 August 2016 through 25 August 2016

ER -

Chan HL, Norrish M. Proof pearl: Bounding least common multiples with triangles. In Blanchette JC, Merz S, editors, Interactive Theorem Proving - 7th International Conference, ITP 2016, Proceedings. Springer Verlag. 2016. p. 140-150. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). doi: 10.1007/978-3-319-43144-4_9

Proof pearl: Bounding least common multiples with triangles

Abstract

Publication series

Conference

Access to Document

Other files and links

Fingerprint

Cite this