Cruise Song

Cruise Song

PhD Student in Computer Science at 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 first-year PhD student in Computer Science at Georgia Institute of Technology, advised by Prof. Vijay Ganesh. Before that, I obtained my B.S. degree in Mathematics and Computer Science from 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

While I am still exploring what is out there in the world of mathematics and computer science, I have been broadly interested in formal methods, particularly the following topics:

  • Formalization of Mathematics.
  • Interactive Theorem Proving.
  • Automated Reasoning.
  • All Possible Combinations of above.
Ramsey (5,3) > 13
R(5,3) > 13. Visualized by a Lean Widget I wrote :D

Mathematical proofs are often complex, and ensuring their logical soundness is a significant challenge. My research addresses this by applying powerful tools like proof assistants and SAT solvers to help formalize mathematics. This means creating machine-checkable proofs, which can enhance reliability and rigor in mathematical research. The very same technique can be applied to ensure the correctness of critical softwares/ systems, or AI (who knows).

More recently, I am working on combining Lean4 and SAT solvers. I am always happy to chat and collabrote :D

News