2017-4-19 阿布瑞尔报告会新闻稿

An exercise in mathematical engineering: Proving weak and strong Goodstein theorems

数学工程中的一个练习：证明弱Goodstein定理和强Goodstein定理

报告题目：An exercise in mathematical engineering: Proving weak and strong Goodstein theorems

报告人：Jean-Raymond Abrial 院士/教授

主持人：朱惠彪

报告时间：2017年4月19日（周三）13:30~14:30

报告地点：中北校区数学馆201

报告人简介：

简-埃蒙德 阿布瑞尔(Jean-Raymond Abrial)，法国计算机科学家，欧洲科学院院士，苏黎世联邦理工学院教授、华东师范大学紫江教授。他是安全攸关软件开发领域的主要奠基人，是将软件形式化方法成功应用于工业界的先驱者。阿布瑞尔教授荣获2015年度上海市国际科技合作奖和2016年度中华人民共和国国际科学技术合作奖。

报告摘要：

多年来，我一直致力于通过correct-by-construction方法研究应用于大型计算机化系统开发的技术。同时，我也在世界各地把这些教授给了许多学生。这个方法最重要的一点就是要通过使用一些工具，来掌握形式化证明。因此我发现，先给学生做一些证明方面的引入这很重要。在介绍完相关背景后，我发现接下来最好的方式就是给学生介绍一些重要的已经完成的纯数学证明。但是数学课本里的一些发现令我有些感到失望。课本里当然有很多证明，但是我发现数学家并没有过多的解释他们是如何发现和得到这个证明的。所以，我决定自己来做。这就是我所说的“数学工程”：尝试深入解释证明中使用的方法。我还发现，这离形式化的系统开发想要完成的并不是太远。在我研究过的证明中，有一个是由Reuben Goodstein在1944年提出的一个反直觉的定理。在这次研讨会中，我将介绍和解释这个定理。

阿布瑞尔（Jean-Raymond Abrial）讲座海报

报告现场