Experimental Math Lab at UD

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.

Getting familiar with LEAN

  1. Level 1: LEAN Game
    It's easy to get addicted! Natural Number Game.
  2. Level 2: Install LEAN
    Follow the directions here (or you can use the online version).
  3. Level 3: Math in LEAN
    Explore the interactive book: Mathematics in Lean.
  4. Level 4: LEAN Math Library
    Check it out on GitHub: Buzzard's 2023 course on Formalizing Mathematics.

    5. Current Projects

    1. Project 1: Homology in (Infinite)-Dimensional Function Spaces
      This is a Capstone project(Spring 2025) by UD undergrad Gabe Gray, directed by Jun Li, exploring advanced mathematical concepts from function spaces and their formalization.
    2. Project 2: 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).