Completed full Lean formalization of the Hamilton–Perelman proof of Thurston’s Geometrization conjecture (beyond Poincaré) with the Humanfia team and collaborators (Geometry library, Humanize, Post).
Regained first place on the LeanEval leaderboard with updated Humanize workflows after ICLR (Leaderboard, Post).
KDA optimized Kimi Delta Attention kernels up to 2.96× over FlashKDA (with Humanize2 / Flame Chase); also helped Databricks reach #1 across SolExecBench tracks in about one week (Details, KDA).
Powered by Humanize + Kimi-K3, achieved a perfect score (6/6, 42/42) on IMO 2026 Lean formal proofs in one run at lower cost than GPT-5.6 (Results, Post).
Presented about token maxing with Humanize at NVIDIA, invited by SGLang (Slides, Talks).
KDA (Kernel Design Agents) powered HAN Lab Kernel Mafia to #1–#3 rankings (MoE, DSA, GDN) in the Pure Agent track of the MLSys FlashInfer Kernel Contest, with minimal prior CUDA experience (Post, KDA).