数学与形式化转向
Mathematics and the formal turn
AI总结：
本文围绕20世纪初确立的数学形式化基础，介绍计算证明助手实现数学知识数字化编码的作用，并列举相关技术助力数学研究的多种途径。
摘要：
自20世纪初以来，人们已认识到数学定义与证明可在具备精确语法与使用规则的形式系统中表示。基于这一基础，计算证明助手如今已能将数学知识以数字形式编码。本文列举了此类及相关技术助力数学研究的若干方式。
英文摘要：
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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
