Welcome to the Experimental Math Lab at the University of Dayton! This platform provides UD math, computer science, and engineering students and faculty with hands-on experience in formal verification, computer-assisted proofs, and AI-based mathematics. This is partially funded by Jun Li's NSF LEAPS grant, to fulfill the education component and provide a inclusive approach for STEM students at UD.
Our projects involve LEAN, a type-theoretic computer language designed to formalize mathematical proofs. LEAN's ultimate goal is to leverage AI in aiding mathematical proof writing and discovery. This emerging field lies at the intersection of computer science and mathematics, offering numerous open questions and clear pathways for impactful contributions. Install LEAN Follow the directions here (or you can use the online version).
Getting familiar with LEAN
-
Level 1: LEAN Game
It's easy to get addicted! Natural Number Game. -
Level 2: Math in LEAN
Explore the interactive book: Mathematics in Lean. -
Level 3: LEAN Math Library
Check it out on GitHub: LEAN 4 Math Library. -
Project 1: Homology in (Infinite)-Dimensional Function Spaces
This is a Capstone project(Spring 2025) by UD undergrad Gabe Gray(Math and CS majors), directed by Jun Li, exploring advanced mathematical concepts from function spaces and their formalization. The project will focus on the formalization in infinite-dimensional function spaces, such as the space of smooth functions on a compact manifold. This will involve developing a rigorous framework for defining chain complexes, homology groups, and homotopy equivalences in the context of function spaces, with the goal of setting up Frechet spaces using the Lean proof assistant. By doing so, this project aims to bridge the gap between infinite dimensional analysis, topology, and formal verification. -
Project 2: Complex Linear algebra, quantum states, and transformations
This is a Capstone project (Spring 2025) by UD undergraduate Will Hach (a double major in Physics and Electrical Engineering), directed by Jun Li. Will was recently admitted to a master's program in optics and has a strong interest in quantum information. The project will focus on the formalization of the mathematics behind quantum information, including the formalization of complex linear algebra, cryptography, quantum states, and fast Fourier transformations in Lean. The ultimate goal is to formalize Shor's algorithm; along the way, we will include various statements in the LEAN library, such as quantum Fourier transform is a unitary transformation, etc. There are interchangeable components with the aforementioned project, and we will also explore the formalization of Lie groups and Lie theory in Lean. -
Project 3: Homotopy Type Theory (HoTT) and Applications in Lean
This project is a Capstone by UD undergrad Joseph Kopp (Math and Physics majors), exploring Homotopy Type Theory (HoTT), the foundational framework of the Lean proof assistant, with the goal of uncovering and developing new “types” for formalizing advanced topological and geometric results. It will utilize core HoTT concepts such as the univalence axiom and higher inductive types, building upon existing Lean libraries to bridge classical algebraic topology with computer-aided proof techniques. By doing so, this project aims to expand the scope of formal verification and encourage the integration of cutting-edge theoretical methods into practical, machine-assisted proofs. -
Project 4: Formalize Smale sphere mapping theorem
We will apply the above function space formalization to prove Smale sphere mapping theorem that the diffeomorphism group of the 2-sphere retracts to O(3). It will use the infinite-dimensional function space formalization to prove the theorem in Lean, together with new types and tactics developed in the above projects.
Current Projects
The following projects will fill the blanks in the LEAN4 undergraduate math library , with a long-term goal of formalizing the moduli of riemann surfaces, Teichmuller theory and mapping class groups in LEAN4.