Euler's Partition Theorem

Euler’s Partition Theorem states that the number of partitions with only distinct parts is equal to the number of partitions with only odd parts. The combinatorial proof follows John Harrison’s pre-existing HOL Light formalization [1]. To understand the rough idea of the proof, I read the lecture notes of the MIT course 18.312 on Algebraic Combinatorics [2] by Gregg Musiker. This theorem is the 45th theorem of the Top 100 Theorems list. Contents 1 Additions to Isabelle’s Main Theories 2

• Type: Journal
• Year: 2015
• Where: AFP
• Authors: Lukas Bulwahn
• Keywords: AFP 2015, Formal Methods