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