NULL

Overview

My repository for my work with the Northwestern Undergraduate Lean Lab. Supervised by Dr. Erin Griffin and Dr. Martin Bishop.

Currently working on contributing to Mathlib and Formal Conjectures

Building

lake exe cache get
lake build

Contents

• almostperfectnum.lean — Formalizing conjectures about almost perfect numbers (Formal Conjectures #2240)
• NULL.lean - Some scratch work and examples
• aliquot.lean - Theorem on boundedness of aliquot sequences