news
| 03/2026 | Started collaborating with the Huawei Noah’s Ark Lab RL team on reinforcement learning and formalisation. This work includes LeanPolish, a kernel-verified symbolic compression framework and dataset for Lean 4 proofs, and CovCal, a risk-controlled Lean-as-judge framework for natural-language mathematical reasoning. |
|---|---|
| 01/2025 | Started contributing to Project Numina on formal reasoning and automated theorem proving. Check out Kimina Prover. |