This page includes other things that I am interested in.

Lean

Lean is a programming language and theorem prover which can be used to formalize theorems in mathematics. Large portions of mathematics have already been formalized in Lean’s mathematical library, Mathlib, and work is ongoing to expand this. The Natural Number Game is a fun game that teaches some of the basics of Lean. My activities in Lean include participating in UNL’s Lean Learning League, contributing to Mathlib, and developing some independent projects that formalize pieces of mathematics of interest to me:

• SymmetricIdeals formalizes a paper on symmetric ideals that I coauthored.
• KostkaNumbers defines Kostka numbers in Lean and proves many results about them and (semi)standard Young tableaux. It includes a formalized proof of the hook length formula (based on the probabilistic proof by Greene, Nijenhuis, and Wilf) and a proof of a key inequality that I used in a paper.
• Lean-Tnorms is a project that formalizes the notion of a triangular norm (t-norm). It proves various properties and structural results about t-norms, roughly following parts of “Triangular Norms” by Klement, Mesiar, and Pap. It also contains a formalization of a paper I wrote on fuzzy logic and the Sorites paradox.

Fuzzy Logic

Fuzzy logic provides a mathematical way to reason rigorously about vagueness. For example, fuzzy logic can be used to resolve the Sorites paradox, which questions when a heap becomes a heap. I recommend this chapter by N. J. J. Smith for an overview of the philsopical side of fuzzy logic. (I find this paper of his on the philsophy of time travel to be very enjoyable and also recommend it, though it has nothing to do with fuzzy logic.)

My interest in fuzzy logic is from the mathematical side. In particular, I like to think about fuzzy logics induced by t-norms and how various properties of the t-norm (e.g. continuity, zero divisors) affect the properties of the fuzzy logic. I’ve written a paper that addresses how properties of the t-norm influence a fuzzy logic’s ability to adequately resolve the Sorites paradox. As noted above, I’ve formalized this paper and other facts about t-norms in Lean.

Combinatorial Game Theory

Combinatorial game theory is the mathematical study of two-player games of pure strategy, including classic games like Tic-Tac-Toe, Nim, and Hex. Although it may seem frivolous, combinatorial game theory is a deep and complicated field of mathematics with lots of beautiful theories. It even has connections to the surreal numbers. As an undergrad, I took a capstone course in combinatorial game theory and wrote an exposition on the Sprague-Grundy Theorem. At UNL, I’ve mentored two students in DRPs on combinatorial game theory.