Customize Consent Preferences

We use cookies to help you navigate efficiently and perform certain functions. You will find detailed information about all cookies under each consent category below.

The cookies that are categorized as "Necessary" are stored on your browser as they are essential for enabling the basic functionalities of the site. ... 

Always Active

Necessary cookies are required to enable the basic features of this site, such as providing secure log-in or adjusting your consent preferences. These cookies do not store any personally identifiable data.

No cookies to display.

Functional cookies help perform certain functionalities like sharing the content of the website on social media platforms, collecting feedback, and other third-party features.

No cookies to display.

Analytical cookies are used to understand how visitors interact with the website. These cookies help provide information on metrics such as the number of visitors, bounce rate, traffic source, etc.

No cookies to display.

Performance cookies are used to understand and analyze the key performance indexes of the website which helps in delivering a better user experience for the visitors.

No cookies to display.

Advertisement cookies are used to provide visitors with customized advertisements based on the pages you visited previously and to analyze the effectiveness of the ad campaigns.

No cookies to display.

0

导语:40多年前,计算机科学家在德国多特蒙德举行竞赛,寻找“忙碌海狸”图灵机。如今,这一难题被一群业余爱好者攻破,数学大佬陶哲轩转发消息表示欣慰,认为这体现了证明助手对于数学研究的协作是多么有用。

正文:

一、难题攻破

经过数十年努力,来自世界各地的20多名业余爱好者使用一款名为Coq证明助手的软件,找到了第五个“忙碌海狸”图灵机:BB(5) =47,176,870。这一成就瞬间令社区沸腾,其中爱尔兰梅努斯大学计算机科学家Damien Woods惊叹:“就像博尔特一样,我很惊讶他们的速度如此之快!”

二、忙碌海狸难题

忙碌海狸难题源于1974年,当时确定了第四个忙碌海狸数。自此,寻找第五个忙碌海狸数成为悬而未决的问题。忙碌海狸数是图灵机在停止之前所能写下的最多1的个数。

三、证明助手助力

此次攻破难题的关键在于使用Coq证明助手软件。该软件证实了数学证明没有错误,使得这一成就得以实现。

四、数学研究规则改变

这一成就对数学研究具有重要意义。它表明,业余爱好者也可以在数学领域取得突破,同时也展示了证明助手在数学研究中的重要作用。

五、忙碌海狸游戏

忙碌海狸游戏由数学家Tibor Radó在1962年发明,旨在将停机问题的本质提炼成更简单的形式。游戏的目标是确定忙碌海狸数BB(n)的确切值。

六、早期挑战者

早期挑战者之一是俄勒冈州立大学数学研究生Allen Brady。他编写了计算机程序来模拟图灵机的行为,并使用一台强大的计算机进行模拟。

结语:

40年图灵机难题被业余玩家攻破,不仅体现了数学研究的无限魅力,也展示了业余爱好者在数学领域的潜力。这一成就将为数学研究带来新的启示,也为数学界注入新的活力。


>>> Read more <<<

Views: 0

0

发表回复

您的邮箱地址不会被公开。 必填项已用 * 标注