在数学中,严谨性至关重要。但数字化的证明是否过于严苛?
In Math, Rigor Is Vital. But Are Digitized Proofs Taking It Too Far?

原始链接: https://www.quantamagazine.org/in-math-rigor-is-vital-but-are-digitized-proofs-taking-it-too-far-20260325/

布尔巴基小组在20世纪深刻地重塑了数学,并非通过新的发现,而是通过对抽象和严格形式化的彻底强调。他们优先考虑一般陈述和逻辑推导,而非直觉和具体例子,创造了一种高度“严谨”且无懈可击的风格,并被广泛采用。 虽然这种方法提高了数学的可靠性和清晰度,但也存在缺点。诸如组合学和图论等领域,依赖于具体的视觉化,最初被边缘化。一些数学家现在担心布尔巴基的成功助长了同质化,通过掩盖替代方法(例如历史上几何的意大利代数几何学派)而降低了数学的“文化多样性”。 目前,新一代数学家正试图使用计算机“证明助手”(如Lean)来实现*真正*的形式化证明,旨在验证每一个逻辑步骤,甚至基本的算术。这个雄心勃勃的项目,在大量资金的支持下,寻求形式化所有数学,并可能解决人类严谨性的局限性。

黑客新闻 新 | 过去 | 评论 | 提问 | 展示 | 招聘 | 提交 登录 在数学中,严谨性至关重要。但数字化的证明是否太过严苛? (quantamagazine.org) 10 分,由 isaacfrond 发表于 2 小时前 | 隐藏 | 过去 | 收藏 | 2 条评论 帮助 riverforest 0 分钟前 | 下一个 [–] 严谨性是数学的全部意义。一旦你开始质疑是否存在过多的严谨性,你就是在解决一个不同的问题。回复 ux266478 27 分钟前 | 上一个 [–] 严谨性从来都不是数学所必需的。ZFC 被明确地推崇为数学的基础,是因为类型论过于严谨和苛求。我认为数学家们正在转向类型论,这是一种被许多人忽视的讽刺。现在我们只需要恢复逻辑主义... 指南 | 常见问题 | 列表 | API | 安全 | 法律 | 申请 YC | 联系 搜索:
相关文章

原文

The real legacy of these books, however, is not their content but their style. Bourbaki prioritized abstraction over all else, eschewing concrete examples and calculations in favor of only the most general statements. They presented each proof as a series of logical deductions, usually without reference to any underlying intuition or rationale.

“It’s a style that is very formal,” said Leo Corry, a historian at Tel Aviv University. “Very austere.”

Bourbaki’s philosophy quickly spread, influencing mathematics almost everywhere. “It had an enormous influence,” said Patrick Massot of Paris-Saclay University. “The most successful parts have become so much part of the common mathematical knowledge and style that it’s hard to think of what it was before.”

The subject became far more airtight, if increasingly abstract and difficult. “This was not a brilliant decision from a pedagogical point of view,” wrote Maurice Mashaal, the longtime editor of Pour la Science and the author of a book on Bourbaki. But the group’s emphasis on abstraction molded research mathematics in ways that are harder to assess.

Some mathematicians revere Bourbaki’s approach. Massot argues that through abstraction and elegance, “you are forced to understand what really makes things work, and what is just noise.” Formalization, in this view, has brought clarity.

But Bourbaki’s project had unforeseen consequences as well. Their vocabulary and style weren’t a natural fit for every type of mathematics. For example, the fields of combinatorics (often described as the science of counting) and graph theory (the science of networks) tend to be highly concrete and visual. Perhaps, then, it’s no surprise that for decades, they were sidelined at most prestigious institutions in the United States and parts of Europe; they were only able to thrive in places where Bourbaki’s influence was limited, like Hungary.

“Graph theory [was] the slum of topology,” said Béla Bollobás of the University of Cambridge. “That atmosphere changed only recently. Very recently.”

Even in fields that did flourish under the Bourbaki framework — algebra, topology, analysis — some mathematicians worry that Bourbaki was too successful. According to them, the ways in which proofs are written and theories constructed have become overly homogeneous.

“There is a sense that it decreased the cultural diversity of mathematics,” said Aravind Asok of the University of Southern California. Before Bourbaki, for instance, there were many versions of algebraic geometry. In France, for example, methods were grounded in analysis, while in Italy, a geometric style reigned.

The Italian school, which lacked rigor and involved many errors, quickly faded as Bourbaki’s influence spread. Certainly, algebraic geometry became more reliable. But by cutting off other paths of possible progress, Bourbaki introduced a new problem. “I don’t want any mathematics where one mode dominates,” Asok said. “There is a cultural history to mathematics that deserves to be preserved.”

Despite the best efforts of Bourbaki, Cauchy, and Weierstrass, truly formal proofs have always been objects of theory, not practice. Some mathematicians now hope that computers can change that.

Since the 1960s, researchers have been developing computer programs called proof assistants. Using a proof assistant, a mathematician will write every line of a proof (including every definition) in a language that the computer can understand, and then the proof assistant will check the logic. If even a single step doesn’t follow from a preceding one — if you haven’t rigorously shown every tiny detail, like the fact that 1 + 1 equals 2 — then the program will not consider the proof correct.

Currently, mathematicians are hoping to formalize all of mathematics using a proof assistant called Lean. They’ve created a library of more than 120,000 definitions so far and have verified a quarter of a million theorems. Several mathematicians maintain this database, keeping it up to date and vetting new contributions. (A handful of them do this work full time.) They’ve received over $10 million in funding, mostly from the billionaire financier Alex Gerko.

联系我们 contact @ memedata.com