中国科学院数学与系统科学研究院研究员，中国科学院国家数学与交叉科学中心执行主任。
主要研究人工智能数学理论、数学机械化、自动推理。主要成果包括：提出了几何约束求解的系统高效算法，将数学机械方法由定理机器证明开拓到自动作图新方向，所提方法被中、美、德、法、英等国学者应用于无人飞行器、无人驾驶、卫星定位、视频监视、工业机器人等多种智能系统；合作建立了几何定理机器证明消点法，首次实现几何定理可读证明的自动生成；合作建立了微分稀疏结式、周形式与差分特征列理论与高效算法，实质性开拓了数学机械化方法的适用范围；在对抗深度学习的数学理论方面取得的重要进展。
曾获国家自然科学二等奖、吴文俊应用数学奖、吴文俊人工智能杰出贡献奖、国际计算机学会SIGSAM/ISSAC杰出论文奖、香港求是杰出青年学者奖。作为首席科学家主持了973项目“数学机械化与自动推理平台”、“数学机械化方法及信息技术应用”、“数学机械化与数字化设计制造”，获科技部“十一五国家科技计划执行突出贡献奖”；
曾主持国家基金委优秀创新群体与国家杰出青年基金。
