Education
- Ph.D. in Computer Science, Georgia Institute of Technology, 2029 (expected)
- B.S. in Mathematics & Computer Science, University of Michigan, 2024
Publications
- D. Narváez, C. Song, N. Zhang.“Formalizing Finite Ramsey Theory in Lean 4”. Accepted to the 17th Conference on Intelligent Computer Mathematics (CICM 2024).
Research Experience
The Polymath Jr Program
Undergraduate researcher | Advisor: Dr. David Narváez (Virginia Tech) | Jun. 2022 - Jun. 2024
- Acquired proficiency with interactive theorem proving using Lean 3 & Lean 4.
- Designed and developed tactics to facilitate manipulation of sets in proofs.
- Formalized exact values for several small Ramsey numbers and related van der Waerden numbers using interactive and automated theorem proving with SAT solvers.
- Developed a graph widget in Lean that interactively visualizes the graphs used in proofs.
- GitHub repository: GitHub - cruisesong7/formal_ramsey
Michigan Aerospace and Robotics Verification Lab (MARVL)
Undergraduate researcher | Advisor: Prof. Jean-Baptiste Jeannin | Jul. 2023 - May 2024
- Familiarized with the Coq proof assistant and studied formal verification on iterative methods.
- Extended the verification on Jacobi methods into Block Jacobi with parallel C program and error bounds derivation in floating-point arithmetic.
- Ported the project into recently released Coq-Mathcomp2 and cleaned up the repetitive proofs by writing Ltac2.
- Read and solved exercises in Software Foundations: Logical Foundations by Benjamin Pierce.
Teaching Experience
Course Assistant, Multivariable Calculus (Math 215)
University of Michigan | Winter 2023
- Provided in-class guidance for students in an Inquiry-Based Learning (IBL) environment.
Tutor, Math Lab
University of Michigan | Fall 2022 - Winter 2023
- Tutored undergraduate level math courses, mainly introductory mathematics courses from Calculus I to Differential Equations, occasionally helping with more advanced courses such as Real Analysis.