标题： 数学与形式化转变 显示英文标题

标题： Mathematics and the formal turn

摘要： 自二十世纪初以来，人们就已认识到数学定义和证明可以表示在具有精确语法和使用规则的形式系统中。在此基础上，计算证明助手现在使以数字形式编码数学知识成为可能。本文列举了这些技术和相关技术可以帮助我们做数学的一些方式。 显示英文摘要

摘要： Since the early twentieth century, it has been understood that mathematical definitions and proofs can be represented in formal systems systems with precise grammars and rules of use. Building on such foundations, computational proof assistants now make it possible to encode mathematical knowledge in digital form. This article enumerates some of the ways that these and related technologies can help us do mathematics.