Cruise Song | Georgia Institute of Technology

About Me

“We must know. We will know.” — David Hilbert

Hi, my name is Cruise (or you might know me as Congyan). I am a second-year Ph.D. student in Computer Science at the Georgia Institute of Technology, advised by Prof. Vijay Ganesh. Before that, I obtained my B.S. in Mathematics and Computer Science from the University of Michigan, where I was fortunate to work with Prof. Jean-Baptiste Jeannin on formal verification of numerical methods. I have also been working on formalizing Ramsey theory with Dr. David E. Narváez, who introduced me to the wonderful field of formal methods.

Research Interests

I am broadly interested in formal verification, particularly the following topics:

Formalization of Mathematics
Verification of Parsers & Compilers
Theorem Proving & Automated Reasoning
Autoformalization & Neurosymbolic AI

Ramsey (5,3) > 13. Visualized by a Lean widget I wrote :D

Formal verification is the pursuit of trust and guarantees for systems ranging from mathematics to software. My earlier work focused on formalizing mathematics such as Ramsey theory with Lean 4 and SAT solvers, producing machine-checkable proofs that bring reliability and rigor to mathematical research.

More recently, I have become interested in the verification of parsers and compilers, where the goal is to guarantee a faithful translation from an input language to an output language. To me, this is what makes verification so compelling: it bridges abstract, high-level intent and its concrete realization in the real world.

News

[2026] Our paper “Just Draw It: Widgets for Generating and Visualizing Graph Structures in Lean 4” was accepted to HATRA 2026, co-located with SPLASH/ISSTA 2026.
[2026] I interned at the Amazon Automated Reasoning group (Verified Permissions) as an Applied Scientist Intern, where I am grateful to work with Dr. Liana Hadarean on verifying Cedar parsers in Lean.
[2025] I spent an amazing summer interning at Imandra, collaborating closely with Dr. Grant Passmore on integrating Imandra-geo into Lean to handle nonlinear real arithmetic.
[2024] My first publication, “Formalizing Finite Ramsey Theory in Lean 4”, was accepted to CICM 2024!
[2024] I attended the Summer School on Formal Techniques, and I highly recommend peers interested in this field to attend!

Publications

Just Draw It: Widgets for Generating and Visualizing Graph Structures in Lean 4

C. Song, Z. Li, S. Binder, V. Ganesh

Workshop on Human Aspects of Types and Reasoning Assistants (HATRA), co-located with SPLASH/ISSTA, 2026.

Project Page
ProofBridge: Auto-Formalization of Natural Language Proofs in Lean via Joint Embeddings

P. Jana, K. Kale, E. Tanrıverdi, C. Song, S. Vishwanath, V. Ganesh

International Conference on Learning Representations (ICLR), 2026.

PDF
Formalizing Finite Ramsey Theory in Lean 4

D. Narváez, C. Song, N. Zhang

International Conference on Intelligent Computer Mathematics (CICM), 2024, pp. 91–108.

PDF