TheReefink

一个致力于为本地人工智能助理打造确定性、经机器证明扩展的业余研究小组 · ghillie，爪本身 →

我们将安全地、确定性地变异我们的爪，并用已证明的代码构建扩展它们能力范围的 工具。一个业余研究小组，取的是业余无线电爱好者那种意义：我们自己的机器，我们 自己的证明，没有什么要求被信任。 为什么组织胜过脑容量 →

三条规则

1. 没有什么要求被信任。 会员所依赖的每一项主张，都必须 是他们自己能够重新推导出的：一份证明、一个摘要、一张真值表。“维护者这么说”不是我们使用 的一种理由类别。
2. 拒绝就是发现。 一份未能证明成立的证明、一个无法读取 的存储、一个被如实记录下来的缺口——这些正是系统在正常运作，它们会被写下来，而绝不会被 抹平。那份无聊的报告——它又一次精确地做到了其定理所说的——同样也是一项发现。
3. 主人的位阶永远高于爪。 扩展可以做决定；但它们永远不会获得权限。无论一项实验能证明什么，都不会改变这一点。

成为其中一员——今天就重新推导你的第一份证明

你不需要账号，不需要注册，也不需要从我们这里拿取任何你无法自行核验的东西。 第一次接触这个？ 从入门路线开始 — 三个步骤，不在你的系统上安装任何东西，并且止步于证明本身。这里接下来的内容是 完整流程。两次下载，十分钟：

1. 获取证明器。 免费的 GNAT FSF 工具链——它把 SPARK 证明器和构建 工具打包在了一起：

https://github.com/alire-project/GNAT-FSF-builds/releases
  (gnatprove-x86_64-linux, -darwin, or -windows64 — unpack anywhere)

仅这个软件包本身，就足以完成第 3 步——重新推导证明。但它不足以完成 第 4 步——构建前端：它自带 gcc 和 ld，却没有 C 运行库，也没有启动对象文件，所以在缺少 这些的机器上，构建会在证明已经成立之后才失败——这是发现缺件的最糟时机。你还需要 binutils 和 libc6-dev。这些是任何 Linux 系统的常规构建必需 品，几乎任何用于开发的机器上早已具备；只有裸容器或全新的最小化安装才会缺少它们。在 Debian 和 Ubuntu 上：

sudo apt-get install binutils libc6-dev
# Fedora/RHEL: the equivalents are binutils and glibc-devel

2. 获取入门扩展。 一个真实的决策核心—— brief-fill policy，决定一个助理何时可以代替主人回答——以附带证明与完整真值表 的源码形式提供：

3. 重新推导证明。 从解包后的包中：

cd brief-fill-policy/core/src
gnatprove -P proof.gpr -f -U --level=2
# success: "0 unproved" — four named theorems, discharged on YOUR machine:
#   NEVER-FILLED-WITHOUT-A-LICENSING-RULE
#   AN-ABSENT-STORE-NEVER-LETS-A-FILL-THROUGH
#   NOTHING-INVENTED-EVER
#   NOTHING-ASKED-THAT-A-RULE-ALREADY-ANSWERS

4. 试着打破它。 修改源码，让一个缺失的规则存储也能放行一个回答， 然后再次运行证明器。它会拒绝——并指出你违背的确切定理。这个拒绝就是整个安全模型，而你 刚刚亲眼看到它在不需要信任任何人的情况下运作。接下来构建前端，并核对其附带真值表的每 一行（包内的 core/REPROVE.md 会引导你完成这一步）。

目标

要达到这样一个位置：我们的聪明才智与协作，使我们的 token 与我们的推理成为当下可得 的最好的——并让每一位会员实质上都变得极其富有。富有的是这里真正重要的那种货币：被证明 的推理是像图书馆一样复利增长的，而不是像一块饼那样分掉——每加入一个核心，都会让每一位 会员更富有，且不损及任何人；直到一个普通会员的爪所掌握的、可核验的能力，超过金钱所能租 到的一切。

为什么这份工作被称为 Wu

工厂的工作单位——一条从一句朴素的话锻造而成的、已被证明的规则——被称为一个 Wu， 得名于吴健雄。

1956 年，杨振宁与李政道提出了一个宏大的问题——大自然分得清左右吗？——一个当时几乎 所有人都认为不值得问的问题。而回答它的，是吴健雄的实验——她的设计、她的装置、她的测量。 次年的诺贝尔奖，只颁给了两位理论家。那个问题配得上这份奖项；那个答案同样配得上，而答案 被漏掉了。

这个故事的两个部分都活在这里。那个被坦率提出的大胆问题，是我们每一项工作的起点—— 我们敬重杨振宁，也效仿他。但我们以吴命名工作单位，因为证明才是工作本身：不是想法，不是 宣告——而是被证实、可核验的结果。而我们公开以她命名，是因为我们知道那个做出证实的人有 多容易被抹去，而在这里，这不会发生。

即将到来的

• 终端——这些扩展所服务的爪：一个没有监听端口、也没有入站路径的本 地助理（它只向外轮询；没有任何东西能进来），每一项要紧的决定背后都有一个已证明的核心。 开源（AGPL-3.0）——已发布：源码与二进制文件在 github.com/the-dark-factory/Ghillie_AGPL。 运行之前先核验二进制文件：发行版附带 SHA256SUMS-assets.txt，它覆盖的正 是你下载到的压缩包本身，因此 sha256sum -c SHA256SUMS-assets.txt 就能 按原样核验它们。（较旧的 SHA256SUMS 仍然保留，供曾经引用过它的人使用； 它以带平台前缀的格式列出解包后二进制文件的摘要值，sha256sum -c 无法读取这种格式。）
• 目录已经上线——一个正在运行的 ghillie 会安装那些在它自己机器上重新证明的扩展：ghillie -catalogue https://thereef.ink/catalogue -abilities-available， 然后 -get-ability <name> -reprove。除非证明先在你自己的硬件上成 立，否则什么都不会安装。
• 目录——更多同样形态的、可重新证明的扩展：安静时段、支出上限、 联系人授权、口径规则（拒绝从不会被改写措辞），每一项都有各自命名的定理。
• 合作社——共享的缺口记录簿，让一只爪记录下的盲点，成为所有爪的 先见；以及汇集的证明工作：证明是唯一一种你可以安全地接受陌生人来做的工作量，因为一次 证明的成立，要么能被重新推导出来，要么不能。

报告

跑过这份证明了吗？礼貌地打破过什么吗？发现过那个无聊的结果吗？写信到 tonythegair@gmail.com。发现会被公开发 布；除此之外不会向你索取任何其他信息——这个页面没有脚本、没有 cookie、也没有统计分析， 你可以通过阅读它来核实这一点。向你送出这个页面的服务器，确实会为每次请求保留一行简短 的、经截断的记录，我们也坦白地这样说：服务器记录了什么。

赞助

TheReefink 由 The Dark Factory Ltd 赞助，该公司已投入相当可观的 资源来促成它的成功——证明所需的机械装置、最早的一批扩展，以及即将到来的终端。这份赞助 买不到任何例外：赞助方在这里发布的一切，都要接受和其他所有东西一样的规则核验，而一位 礼貌地打破它的会员，就是为这个小组做了一件好事。