Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] new in the AFP: Cardinality of Number Partitions


view this post on Zulip Email Gateway (Aug 22 2022 at 12:32):

From: Lawrence Paulson <lp15@cam.ac.uk>
The first AFP entry for 2016 is now online:

http://afp.sourceforge.net/entries/Card_Number_Partitions.shtml

This entry provides a basic library for number partitions, defines the
two-argument partition function through its recurrence relation and relates
this partition function to the cardinality of number partitions. The main
proof shows that the recursively-defined partition function with arguments
n and k equals the cardinality of number partitions of n with exactly k parts.
The combinatorial proof follows the proof sketch of Theorem 2.4.1 in
Mazur's textbook Combinatorics: A Guided Tour. This entry can serve as
starting point for various more intrinsic properties about number partitions,
the partition function and related recurrence relations.

Many thanks to Lukas Bulwahn for this contribution!

Larry


Last updated: Apr 25 2024 at 12:23 UTC