🏆🏅祝贺我组袁野、刘成武（目前在华为实习）两位博士领衔，大四保本组硕士的李思齐，以及实习生谢佳璇 、李博涛几位同学组队，获得CCF LLMLean形式化数学竞赛比赛一等奖，还给我带来一个优秀指导老师奖。
这个团队已经持续在ACL、ICML、ENMLP等顶会发表高水平论文。

北⼤华为的这⼀突破性成果，不仅为中国在AI形式化推理领域赢得了荣誉，更为⼤模型在严谨数学证明这⼀“最后堡垒”的攻克提供了可⾏的技术路线。
随着openPangu等国产⼤模型的持续进化，我们有理由期待AI在数学研究、科学发现、教育辅助和软件验证等领域扮演越来越᯿要的⻆⾊。形式化数学证明这⼀曾经被认为是AI“禁区”的领域，正在被中国科研团队⼀步步攻克。

“能⼒互补优于盲⽬扩⼤计算，分解式严格对⻬优于宽松验证。 ”——这不仅是“Lean说的都队”的技术哲学，或许也是AI攻克形式化数学证明这⼀终极挑战的可⾏路径。