科技与数学小故事

故事1倒着走回去

想象一下，小林在玩寻宝游戏。纸条上写着一道题：“一个数，先加上 5，再乘 2，结果是 30。这个数是几？”

小林从前往后试。试 5：5 + 5 = 10，10 × 2 = 20，太小了。试 8：8 + 5 = 13，13 × 2 = 26，还差一点。

旁边的小周说：“我们从终点往回走吧！”

最后一步是“乘 2”，得到 30。所以乘 2 之前的数，是 30 的一半：30 ÷ 2 = 15。

再往前一步是“加 5”，得到 15。所以加 5 之前的数是：15 − 5 = 10。

小林把 10 放回题里检查：10 + 5 = 15，15 × 2 = 30。对了！

有一位作者常写关于学数学的文章。他最近在读一份报告，讲的是“人是怎么学习的”。报告里说，解题有两种走法。一种是从知道的条件出发，往前推。另一种是从要找的答案出发，往回推。

报告还说，会做一道题还不够。要能把学过的方法，用到没见过的新题上。

“倒着走”就是一个能带着走的好方法。往回走时，每一步都做相反的事：加变成减，乘变成除。

故事21600 万行的数学城

数学家会写“证明”。证明就是一步一步说清楚：一件事为什么一定是对的。证明写得很长时，人看的时候可能会看漏。

有一种电脑语言叫 Lean。用它来写证明，电脑就能一步一步地检查。

据报道，有一家公司叫 Axiom。他们让 AI 在人的看管下，做了一件大事：把一整套数学资料，全部改写成了 Lean 代码。这套资料叫 Stacks Project，讲的是一门很深的数学，叫代数几何。

他们一共写了大约 1600 万行代码。每一行都经过了 Lean 的检查。这些代码免费给大家用。他们把它叫作“一座数学之城”。这条消息在网上被看了大约 430 万次。

1600 万行有多少呢？我们来算一算。假如一个人每天能认真读完 1000 行，16000000 ÷ 1000 = 16000，要读 16000 天。一年按 365 天算，16000 天大约是四十多年。

为什么叫“城”？这是一个比方。一行行代码像砖块，砖块搭成房子，房子连成街道。这些砖不是每一块都靠人搬的，但是每一块都被检查过。