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

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

• Formalization of Mathematics.
• Interactive Theorem Proving.
• Automated Reasoning.
• All Possible Combinations of above.

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 such as cryptographic protocols.

One of my primary research interest is Ramsey theory, a cornerstone of extremal graph theory. I noticed that proving Ramsey-theoretic theorems often requires extensive computation, a task where interactive and automated theorem proving communities could benefit from closer collaboration. My work since then has focused on integrating the strengths of both fields to tackle these challenges. For example, automated reasoning engines can be embedded into interactive theorem provers via metaprogramming, while interactive theorem proving can provide the trustworthy domain knowledge that benefits an automated prover’s search.

News

• I spent an amazing summer interning at Imandra, where I collaborated closely with Dr. Grant Passmore on intergrating Imandra-geo into Lean to handle nonlinear real arithemtic. Watch out for our public release!
• My first publication “Formalizing Finite Ramsey Theory in Lean 4” was accepted to CICM 2024!
• I Attended the Summer School on Formal Techniques, and I highly recommend my peers interested in this field to attend!