初等微分几何的机械化证明

定理证明是数学逻辑推理表现形式的主要环节。它依赖于人脑的主观活动,由于它的规律性没有被充分认识而变得十分困难,以致数学家们的绝大部份精力时间往往都消耗在这上面。现代数学中数理逻辑的发展,已经指出逻辑推理可成为犹如数值计算那样有确切规律可循的过程。