About Me

Hi, I'm Chris Su

Background

Welcome to my personal page!

I'm currently an undergraduate student at Carnegie Mellon University, where I study artificial intelligence and computer science.

My interests are in machine learning, software engineering, and theoretical computer science.

I like nature and animals, with my favorite animal being the polar bear. My favorite fun fact is that llamas and cows don't have upper front teeth!

Interests/Experience

More recently, I've been interested by the theorem proving / functional programming / compilers space1. One of the main projects I hope to take up in the future is writing the Lean4 kernel in OCaml2 as well as formalizing some theorems in complexity theory once Lean4 figures out cost models for program analysis3.

In the past / currently, I've worked on the following:

• present Recently joined @Stagira Labs working on software in the intersections of formal methods, game theory, and rl.
• present Controls software engineer @ Carnegie Mellon Racing Driverless, where I work(/ed) on improving simulation software and reducing testing hours + deep reinforcement learning and control theory. We build autonomous racecars and we're one of the pioneering teams for collegiate competitive autonomous racing in the US!
• present Building elastisched, a data-driven task scheduler and event calendar. It can learn your task habits, preference-learn the ways you want your tasks to be scheduled, and integrates with common calendar providers. Read more about it in the github!4
• 2025 (summer) SDE intern @ Amazon Ads, where I built a validation stack for validating rankings/recommendations models + did some cool statistical studies
• 2024 (summer) REU program @ ASU Sensip Center for convnet dimensionality reduction using quantum computing
• 2022-2023 Software intern @ Acivilate, inc., a gov-tech startup for reducing recidivism

Random goals

• Learn how to make su-jeong-gwa
• Learn the PCP Theorem
• Learn Lean4
• Learn 日本語 (japanese!)

Bleu

Since the end of 2023, I began semi-frequently posting on my ai / complexity theory blog, bleu. The name of the blog comes from french for blue, which is my favorite color. It's also inspired by name of the BLEU (Bilingual Evaluation Understudy) metric, which was/is used to study the faithfulness of machine translations between languages.

Last month (December 2025), the blog turned 2 years old (birthday post coming soon...)! The content of the blog was initially motivated by CMU's 15-251, Great Ideas in Theoretical Computer Science, partly by Scott Aaronson's blog, and primarily my interests in theoretical cs.

Here are some of the recent posts!

• 2025-12-01 — revisiting bin. search - reduction to partitioned boolean array search
• 2025-11-15 — toda's theorem - PH is a subset of P^#SAT
• 2025-10-28 — lean is amazing! - lean4 propaganda
• 2025-10-17 — pre training as bootstrapping - llm post-training
• 2025-08-21 — your time is taking up my space! - time travel as a computational resource? (pt 3)

My Links

Connect with me online:

• GitHub
• LinkedIn
• Bleu - my blog!

Get In Touch!

Email: chrisssu19 [@] gmail.com

School email: chrjs [@] cmu.edu

1. I recall writing about how I found it kinda worrying that scientific research has become so specialized that only a handful of experts can really verify papers in the field. (Auto)Formalization to me is one of the most important projects that will break us free of verification bottleneck. Assuming you trust proof assistants, compilable code gets you verification of papers (and results) for free. This makes science modular (like code), at the cost of abstracting away the intuition of an idea/proof, which is often more important than the implications. But, I think this is not that big of a problem, since we can have translations of formal code back into natural language.

2. See here for info about the Lean4 kernel, and here for why this is important and interesting! I may look for a partner to help me with this, and if this interests you, please reach out to me!

3. I *believe* they're close. Last I heard, there was a project called the Boole language for doing CS/algo stuff, but I haven't checked on it in a long time. Some theorems I have in mind are: Cook-Levin theorem, {ambitiously} the PCP theorem (Dinur's proof could work too), or PSPACE=IP.

4. I had originally built this app to help me time-manage and just put tasks on my calendar since I felt I was wasting time scheduling things myself. It has helped me incredibly recently, and I think there's some interesting ways to improve it! I am looking for co-founders/maintainers and have some ideas for the future of this project!