TY - GEN

T1 - Proof pearl

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

AU - Chan, Hing Lun

AU - Norrish, Michael

N1 - Publisher Copyright:
© Springer International Publishing Switzerland 2016.

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 -