1954-09--1959-07   北京大学   学士

   

2011-06~现在,  中国科学院重庆绿色智能技术研究院（筹）, 主任
1995-11~现在, 中国科学院成都计算机应用研究所, 名誉所长
1990-08~1995-10,中科院成都计算机应用研究所 , 研究员、 副所长
1987-01~1990-07,中科院成都分院数理室, 研究员、室主任
1985-05~1986-12,中科院成都分院数理室, 副研究员
1981-07~1985-04,中国科技大学数学系, 副教授
1979-09~1981-06,中国科技大学数学系, 讲师
1954-09~1959-07,北京大学, 学士

   

（1） 好玩的数学, 二等奖, 国家级, 2009
（2） 数学家的眼光, 二等奖, 国家级, 2005
（3） 定理机器证明理论与算法的新进展, 二等奖, 国家级, 1997
（4） 定理机器证明理论与算法的新进展, 一等奖, 部委级, 1995

   

（ 1 ） 非线性代数方程组与定理机器证明, Nonlinear algebraic equation system and automated theorem proving, 上海科技教育出版社, 1996-01, 第 2 作者
（ 2 ） 几何新方法和新体系, 几何新方法和新体系, 科学出版社, 2009-08, 第 1 作者
（ 3 ） 一线串通的初等数学, 一线串通的初等数学, 科学出版社, 2009-08, 第 1 作者
（ 4 ） 直来直去的微积分, 直来直去的微积分, 科学出版社, 2010-05, 第 1 作者
（ 5 ） 普通高等教育"十二五"规划教材·国家精品课程教材·21世纪教育技术学精品教材, 北京大学出版社, 2015-01, 第 1 作者
（ 6 ） 几何定理机器证明的几何不变量方法, 科学出版社, 2015-04, 第 1 作者

   

（ 1 ） 微分代数方程的可信计算理论与性态分析, 负责人, 地方任务, 2012-04--2015-03
（ 2 ） 基于符号-数值混合计算的误差可控算法及其应用, 参与, 国家任务, 2012-01--2015-12
（ 3 ） 基于数值方法的有理数域上准确多元多项式因式分解, 参与, 国家任务, 2012-01--2015-12
（ 4 ） 基于计算机推理的多领域统一工业模型技术, 参与, 地方任务, 2011-09--2013-08
（ 5 ） 基于混合计算的误差可控算法, 参与, 国家任务, 2011-01--2015-12