- 🔭 Working toward a career as an AI GPU compiler engineer
- ⚙️ Writing GPU kernels and compiler experiments: bytes-in-flight, kernel-forge, mini-triton
- 🧮 Formalizing mathematics in Lean 4 / Mathlib and building LeanBench
- 👯 Open to collaborating on ML compilers, Triton and formal verification **
GPU & compilers
| Project | Stack |
|---|---|
| bytes-in-flight | CUDA |
| kernel-forge | CUDA |
| mini-triton | C++ |
| gluon | Python |
| llm_inference_engine | Python |
Formal mathematics (Lean 4)
| Project | What it is |
|---|---|
| LeanBench | Benchmark for evaluating Lean 4 proofs |
| lean-arena | Python tooling around Lean |
| Analysis-I-by-Terence-Tao | Analysis I (4th ed.) in Lean 4 |
| RetosMatematicos | Competition problems formalized in Lean 4 |
| IMO | IMO problems in Lean 4 |
| MathAdv_Lean4 | Lean 4 proofs for MathAdv exercises |
| p-subset-np | Lean 4 proof of P ⊆ NP for the formal-conjectures definitions |