- AI for Quantum Code Compilation
- Lead mentor: Andres Paz
- Members: Eric Hur, Mayee Sun, Sylvie Lausier, Christian Tarta
- Description: Quantum error correction (QEC) codes are traditionally described using stabilizers, which define the subspace preserved by the code. However, implementing these codes requires translating stabilizers into fault-tolerant quantum circuits—an inherently nontrivial task that is highly dependent on the constraints and capabilities of the underlying hardware architecture.
This project aims to develop an AI agent capable of synthesizing such circuits in a way that:
1. In the ideal (noiseless) setting, the resulting circuits implement the intended stabilizer structure of the code on the target architecture.
2. In the noisy setting, the agent searches over circuit variations to optimize fidelity, taking into account realistic noise models and architectural constraints.
The outcome would be a toolchain that bridges the gap between abstract QEC code design and concrete, high-performance circuit implementations, enabling better exploration of architecture-specific tradeoffs in fault-tolerant quantum computing. - Prerequisites: linear algebra (must have), ML experience (recommended)
- Deep learning of number theory
- Lead mentors: Jarod Alper and Junaid Hasan
- Members: Andrew Chen, Claire Xu, Ivonne Zhang, Akhil Srinivasan, Nina Tharamal, Hemkesh Bandi
- Description: The goal is to explore to what extent modern machine learning algorithms (e.g., feedforward neural network, transformers, llms) can learn number-theoretic functions such as modular arithmetic, the Mobius function, or gcd. We can first attempt to replicate results from the literature (e.g., https://arxiv.org/pdf/2502.10335, https://arxiv.org/abs/2308.15594) and then explore our own functions and algorithms. We aim to submit to one of the major ML conferences such as ICML or ICLR.
- Prerequisites: Python (must have), ML experience (desired)
- Formalizing Geometric Measure Theory
- Lead mentor: Ignacio Tejeda
- Members: Annie Cao, Nathan Pao, Theodore Meek
- Description: The goal is to formalizing the following theorem in geometric analysis: If E is a set of Hausdorff dimension 0 < s < 1, the density D^s(E,x) fails to exist at almost every point x of E. This is Theorem 4.2 in Falconer's book Geometry of Fractal Sets. To get exposure with Lean and specifically with analysis in Lean, this project will begin by following Terence Tao's Lean Companion to his Analysis I textbook.
- Prerequisites: Lean (recommended), analysis (recommended)
- Formalizing Stacks
- Lead mentors: Eric Klavins and Max Lieblich
- Additional mentor: Leopold Mayer
- Members: Dowland Aiello, James Martin
- Description: This project seeks to give formal definitions in Lean of the mathematical objects of sites, sheaves, and stacks. While these are sophisticated mathematical objects, their definitions are not hard to internalize axiomatically, assuming a basic understanding of category theory. Building off mathlib's definiton of a category, the first aim is to define a site following the Stacks Project Tag 00VG rather than using mathlib's current definition. The focus here is only formalizing these key definitions, rather than building out a larger mathematical library with lemmas and theorems.
- Prerequisites: Lean (recommended), category theory (recommended)
- How good are language models at Lean?
- Lead mentors: Tyson Klingner and Patrick O'Melveny
- Members: Kaira Nair, Drew Bladek, Xinyue Fu, Bohao Chen
- Description: In an effort to understand the ability of frontier general-purpose large language models at generating Lean code, we will design an evaluation procedure for various Lean tasks such as next step generation or entire proof generation. We will run our algorithms on the existing frontier models to see which LLMs perform the best, providing valuable guidance to the Lean community on which LLMs to use for certain use cases. We will use a scalable architecture so that our algorithms can be rerun when new models or versions are released.
- Prerequisites: ML experience (must have), Lean (recommended)
- Lean error correction with language models
- Lead mentor: Vasily Ilin
- Members: Ajit Mallavarapu, Evan Wang, Simon Chess, Daniel Lee, Siyuan Ge
- Description: With the goal of making Lean easier to use and specifically making errors easier to debug, we will curate a Lean error dataset and train models to correct errors. There are currently large data sets of error-free code, e.g., Mathlib and github repositories, but no existing data sets of common human-made errors. This makes it hard to train LLMs to understand the compiler feedback and fix the errors. We will assemble a dataset of erroneous proofs, the compiler feedback, and the error corrections. We fine-tune Qwen 4B on this dataset. We aim to submit to one of the major ML conferences such as ICML or ICLR.
- Prerequisites: Python (must-have), Lean (must-have), an ML course (useful)
- Time Commitment: at least 10 hours a week for a quarter
- Mathematician's copilot: reliable theorem search
- Lead mentors: Vasily Ilin and Giovanni Inchiostro
- Members: Sophie Szeto, Eric Leonen, Ted Guan, Artemii Remizov
- Description: The broad vision is to apply modern machine learning techniques to facilitate mathematical research. As a first step in this direction, this project seeks to design search algorithms for locating theorem statements. Mathematics is unique in academia of having precise, self-contained statements of knowledge, which we refer to as theorems, but as of yet, there is no reliable tool to find existing theorems. Currently frontier language model like ChatGPT might guess at the correct reference but will hallucinate the specific reference numbering. We will develop a search tool by scraping the arxiv or other mathematical documents (e.g., the Stacks Project), extracting theorem statements, and finally computing embeddings of the text. At inference time, we will compare the cosine similarity of the user query to the theorems in our database (which is similar to the technology powering LeanSearch). We aim to submit to one of the major ML conferences such as ICML or ICLR.
- Prerequisites: Python (must-have) and an ML course (useful)
- Time Commitment: at least 5 hours a week for a quarter
- Monogenic extensions of regular local rings
- Meeting time: 8:30-10:30 am on Tuesdays
- Lead mentors: John Leo and Bianca Viray
- Additional mentor:Bryan Boehnke and Haocheng Cai
- Members: George Peykanu, Sathvik Kurapati, Tianshuo Wang, Xinyi Zhi
- Description: The goal is to add to Lean two lemmas from a recent paper (https://arxiv.org/abs/2503.07846). The first lemma is well known and says that an etale extension of regular local rings is monogenic, i.e., generated by a single element. The second lemma says that an extension of regular local rings that fails to be etale at a unique codimension 1 point is also monogenic.
- Prerequisites: Lean (recommended), commutative algebra (recommended)
- Provable Computation in Lean
- Lead mentor: Dhruv Bhatia
- Members: Annis Wu, Ruslana Korolov, Zeyin Feng, Alan Chang
- Description: While lean has seen extensive use as a theorem proving assistant, its capabilities as a computational programming language have been left underutilized. The goal of this project will be to start filling this gap. Along the way, we will learn the basics of functional programming, monads, and Lean’s meta-programming framework to begin implementing algorithms that can both be run efficiently and be reasoned about. Our main goal will be to implement basic algorithms with applications to linear algebra while also proving (in Lean) correctness of said algorithms.
- Prerequisites: Lean (recommended), metaprogramming in Lean (recommended)
- Reinforcement Learning for Polynomials.
- Lead mentor: Jarod Alper and Michael R. Zeng
- Members: Bhaumik Mehta, Kyle Zhang, Rohan Pandey, Trey Adams, Naomi Morato, Evan Porter, Kaijie Jin
- Description: We will use reinforcement learning to train computers to search for efficient arithmetic circuits computing specific polynomials. This is in some sense a simplified version of proof generation, where computers are trained to search for proofs of theorems, except that in this case the search space is considerably smaller. At the same time, this project may shed some light on some explicit questions in algebraic complexity theory, and specifically the algebraic analogue of P vs NP. Our inspiration is the AlphaZero algorithm for two-player games, which we will adapt to a single-player game. The problem we will attack is to find efficient ways to compute a polynomial f(x_1, ..., x_n) using an arithmetic circuit consisting of + and x gates together with scalar multiplication. Our strategy is to use Monte Carlo Tree Search to train a deep neural network to learn an effective evaluation function (giving a score of how close the current state is from computing the polynomial) and a policy (a probability distribution over the next moves, with higher probability given to moves that simplify the expression). The computer is rewarded when it finds efficient arithmetic circuits. We aim to submit to one of the major ML conferences such as ICML or ICLR.
- Prerequisites: Python (must have), ML experience (must have)
- Teaching a computer to knot
- Lead mentors: Allison Henrich (Seattle U) and Andrew Tawfeek
- Members: Sean Kawano, Abel Mesfin, Nicole Ham, Solden Stoll
- Description: Mosaic diagrams were developed in 2008 by Lomanoco and Kauffman to build quantum knot systems. Since then, the structure of mosaics has been widely studied by many others due to their convenient way of encoding a knot in three-dimensional space as a matrix. In 2014, it was shown by Kuriya and Shehab that mosaics are a complete invariant for tame knots, which are the concrete knots we can make with string in everyday life.
In this project, we will utilize this convenient matrix-encoding of knots to help build and train an AI model to recognize knots through their mosaic representation. To be precise, since knots are fundamentally topological objects with connectivity patterns, we will construct together an appropriate graph neural network and train it together, developing the proper milestones to gauge its progress (e.g. first recognizing connectedness, then number of links, etc.) along the way. - Prerequisites: python experience (must have)
theorem mgf_of_iid
{Y : ℕ → Ω → ℝ}
{Z : ℕ → Ω → ℝ}
(h_meas : ∀ (i : ℕ), Measurable (Y i))
(h_indep : ProbabilityTheory.iIndepFun (fun (i : ℕ) => inferInstance) Y μ)
(hident : ∀ (i j : ℕ), ProbabilityTheory.IdentDistrib (Y i) (Y j) μ μ)
(Z_def : ∀ n : ℕ, Z n = (Real.sqrt n)⁻¹ • (∑ i ∈ Finset.range n, Y i)) :
∀ n : ℕ, n > 0 →
∀ t : ℝ, mgf (Z n) μ t = (mgf (Y 0) μ ((√n)⁻¹ * t)) ^ n := by
intro n hn t
rw [Z_def]
rw [ProbabilityTheory.mgf_smul_left]