Winter 2023 Projects
Lean Learning Lab
Faculty Mentor: Dr. Jarod Alper
Project Description: Meeting on Wednesdays from 5-6 pm, the Lean Learning Lab (LLL) is dedicated to formalizing mathematics with the Lean Theorem Prover. Lean is a programming language that allows you to verify the proofs of mathematical statements. At the same time, Lean provides high-level tactics that can also assist you in writing proofs by having the computer itself fill in annoying technical details and computations. Theorem provers such as Lean are changing how mathematical research is done so you might as well get on board now!
The main goal of this project is to learn the functionality of Lean by formalizing various exercises and theorems in undergraduate mathematics. As we get better at Lean, we may endeavor to formalize interesting foundational results (e.g. Hilbert’s 1890 proof of the finite generation of invariant rings) and perhaps even contribute to the growing mathematical library of Lean.
Depending on your background and interests, you can choose the mathematical results that you work toward formalizing. To see whether this might be the right project for you and to get started learning Lean, you can play the “Natural Number Game” (https://www.ma.imperial.ac.uk/~buzzard/xena/natural_number_game/).
Project Level: Intermediate: students who have taken Math 300
Additional Course Requirements:
Programming Requirements: Experience with programming is certainly helpful but not required. We will learn the Lean programming language together.
Analyzing Divination Systems as Cryptographic Random Number Generators
Faculty Mentor: Dan Shumow
Project Description: Divination systems, such as Astrology or Tarot, have been used though out human history, in cultures across the whole world. Though they are based in outdated understanding of the universe, rooted in religion and superstition they have remained popular. Astrology is based on the positions of the sun, moons and other planets in our solar system relative to constellations (distant stars), Tarot is like a deck of cards, and the divination technique follows a regular pattern of drawing cards. This can be viewed as analogous to cryptographic pseudorandom number generators, which provide randomness to cryptographic algorithms and protocols, and how they extract randomness from the environment
This project is interested in looking past the unscientific origins of these systems, and instead seek to characterize the system as a deterministic system that takes readings from the environment. Then these algorithms will be analyzed to see if they provide the desired security properties that a cryptographic random number generator does.
This project also provides an opportunity to make graphical representations of the systems involved, such as the mapping of the actual solar system onto the astrological system.
Project Level: Open: students who have taken Math 126
Additional Course Requirements:
Programming Requirements: Basic programming skills such as Python or using Sage would be good, but not required if the student has Math 300 or above.
Symmetric Group Actions and Applications
Faculty Mentor: Dr. Sara Billey
Project Description:
Following up on fall quarter’s special topics course in “Symmetric Group Representation Theory”, we have discussed three open problems and some related literature. Our main focus has been advancing the notion of Graph Modules introduced by Daniel Brosch in his 2022 Ph.D. thesis. Brosch identified these modules as useful in studying problems in Optimization following the work of Raymond-Saunderson-Singh-Thomas and Gatermann-Parrilo. His focus has been on decomposing graph modules into a direct sum of permutation modules. We have been considering the finer decomposition into irreducible S_n modules, connections to matroids, and connections to the enumeration of isomorphism types of graphs.
Project Level: Advanced: students who have taken multiple upper-level mathematics courses
Additional Course Requirements: Math 480 fall 2022
Programming Requirements: