Formalizing some Historical Partition Theory Identities in Lean

Formalizing some Historical Partition Theory Identities in Lean

    Presenter(s)

    Gabriel Gray

    Comments

    9:00-9:20, Kennedy Union 331

    Description

    Lean is a functional programming language that serves as a proof-checking language to assist mathematicians in the process of writing and confirming mathematical theorems. Particularly, the project taken on by the Lean community is to formalize theorems and definitions from all different areas of math, in pursuit of perhaps a new paradigm and era of mathematical theorem proving. As of right now, much of the work of the Lean community is focused on formalizing all undergraduate and intro-level graduate mathematical content to set the stage for future and more advanced work within the language. Euler's classic partition identity states that the number of partitions of a natural number n into odd parts equals the number of partitions of n into distinct parts. Since then, there have been many extensions, analogs, and generalizations of this famous identity. For example, Glashier in 1883 generalized odd to non-divisible by k, and distinct to appearing less than k times. Currently, the only partition identity formalized within the Lean language is Euler's original identity, leaving a large gap in the area including many historical theorems. This project seeks to do just that; formalizing results such as Glashier's and further extensions, reaching out to newly proven research by the presenter.

    Publication Date

    4-23-2025

    Project Designation

    Capstone Project

    Primary Advisor

    Jun Li

    Primary Advisor's Department

    Mathematics

    Keywords

    Stander Symposium, College of Arts and Sciences

    Institutional Learning Goals

    Scholarship; Practical Wisdom; Community

    Formalizing some Historical Partition Theory Identities in Lean

    Share

    COinS