Announcement_8

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.