数学形式化的现实意义
四十年前,袁萌主张数学形式化,为此,奔走大江南北,科普于全国知名高校之间,收效甚微。
十八大之后,又提此事,有文章可证。当今,已经进入十九大新时代,再次提出数学形式化这个老问题,期望引起社会共鸣。
再过几年,我国进入小康社会,人们期盼更好的生活,更加现代的文化氛围。只懂得几何、三角、代数的高中生,整天玩弄智能手机,而不懂得其中的数学“道理”,显然很不合时宜。
回顾历史,1879年,德国数学家弗雷格(Frege)开启了数学形式化的新时代。随后,一百年来,数学家前仆后继,继续努力,至今创造了当今的互联网智能时代。
大家知道,国外,计算机辅助“数学证明器(软件)”已经上市。大规模集成电路的优化设计不能缺少这种“数学证明器”(Prover)的帮助。智能手机就是一块集成电路板,外壳只是美化摆设而已。
老实说,现代微积分中的“无穷小”是一种高度抽象的形式化数学概念,没有形式化数学(模型论)处理是绝对不行的。中学生能够接受这类抽象概念吗?这就涉及到具体的教学方法问题了。我们多年倡导的(非标准)无穷小微积分就是这种教育方法(国外实践已经证明有效)。
现在的实际情况是,中学毕业生是微积分文盲,大学生是微积分“小糊涂”。长期以往,谈何建设社会主义强大国家?
袁萌 陈启清 1月17日