Education

Selected Coursework: SAT and SMT Solvers, Software Analysis and Test, Programming Languagues

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).

Formalizing Finite Ramsey Theory in Lean 4
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

Formal Verification of Numerical Methods in Coq
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 Assistant, CS4510 Automata and Complexity Georgia Tech | Spring 2025
Course Assistant, Math 215 Multivariable Calculus University of Michigan | Winter 2023
Tutor, Math Lab University of Michigan | Fall 2022 - Winter 2023