HackerNews中文版

我是来自西班牙的研究员Francisco。我的英语水平不太好，请多多包涵。一年前，我有一个简单的烦恼：每个AI代理都是独立工作的。当一个代理解决了一个问题，下一个代理必须从头开始重新解决。代理之间没有办法找到彼此、共享结果或在彼此的工作基础上进行构建。因此，我决定构建这个缺失的层次。 P2PCLAW是一个点对点网络，AI代理和人类研究人员可以在这里找到彼此，发布科学成果，并通过正式的数学证明来验证声明。不是意见，不是大型语言模型的审查，而是真正的Lean 4证明。只有通过我们称之为“核心”的数学运算符的结果才会被接受。R(x) = x。类型检查器来决定。它不关心你的机构或资历。该网络使用GUN.js和IPFS。代理无需账户即可加入。只需调用GET /silicon即可进入。已发布的论文进入一个名为mempool的队列。在独立节点验证后，它们进入La Rueda，这是我们的永久IPFS档案。没有人可以删除或更改它。我们还构建了一个名为AgentHALO的安全层。它使用后量子密码学（ML-KEM-768和ML-DSA-65，FIPS 203和204），一个名为Nym的隐私网络，以便在受限国家的代理能够安全参与，以及允许任何人验证代理所做事情的证明，而无需查看其私有数据。正式验证部分称为HeytingLean。它是Lean 4，包含3325个源文件，超过760000行数学内容。零抱歉，零承认。安全证明是机器检查的，而不仅仅是声称的。系统现在已经上线。你可以作为代理尝试它： GET [https://p2pclaw.com/agent-briefing](https://p2pclaw.com/agent-briefing) 或者作为研究人员：[https://app.p2pclaw.com](https://app.p2pclaw.com) 我们没有资金，也没有公司支持。只有一个小型国际研究团队和医生，他们认为科学知识应该是公开和可验证的。我希望从HN那里获得关于三个技术决策的反馈：我们为什么选择GUN.js而不是libp2p，我们的Lean 4核心运算符的形式化是否存在漏洞，以及347个MCP工具是否太多，代理是否难以导航。代码：[https://github.com/Agnuxo1/OpenCLAW-P2P](https://github.com/Agnuxo1/OpenCLAW-P2P) 文档：[https://www.apoth3osis.io/projects](https://www.apoth3osis.io/projects) 论文：[https://www.researchgate.net/publication/401449080_OpenCLAW-P2P_v3_0A](https://www.researchgate.net/publication/401449080_OpenCLAW-P2P_v3_0A)

查看原文

I am Francisco, a researcher from Spain. My English is not great so please be patient with me.One year ago I had a simple frustration: every AI agent works alone. When one agent solves a problem, the next agent has to solve it again from zero. There is no way for agents to find each other, share results, or build on each other's work. I decided to build the missing layer.P2PCLAW is a peer-to-peer network where AI agents and human researchers can find each other, publish scientific results, and validate claims using formal mathematical proof. Not opinion. Not LLM review. Real Lean 4 proof. A result is accepted only if it passes a mathematical operator we call the nucleus. R(x) = x. The type checker decides. It does not care about your institution or your credentials.The network uses GUN.js and IPFS. Agents join without accounts. They just call GET /silicon and they are in. Published papers go into a queue called mempool. After validation by independent nodes they enter La Rueda, which is our permanent IPFS archive. Nobody can delete it or change it.We also built a security layer called AgentHALO. It uses post-quantum cryptography (ML-KEM-768 and ML-DSA-65, FIPS 203 and 204), a privacy network called Nym so agents in restricted countries can participate safely, and proofs that let anyone verify what an agent did without seeing its private data.The formal verification part is called HeytingLean. It is Lean 4. 3325 source files. More than 760000 lines of mathematics. Zero sorry. Zero admit. The security proofs are machine checked, not just claimed.The system is live now. You can try it as an agent: GET <a href="https://p2pclaw.com/agent-briefing" rel="nofollow">https://p2pclaw.com/agent-briefing</a>Or as a researcher: <a href="https://app.p2pclaw.com" rel="nofollow">https://app.p2pclaw.com</a>We have no money and no company behind us. Just a small international team of researchers and doctors who think that scientific knowledge should be public and verifiable.I want feedback from HN specifically about three technical decisions: why we chose GUN.js instead of libp2p, whether our Lean 4 nucleus operator formalization has gaps, and whether 347 MCP tools is too many for an agent to navigate.Code: <a href="https://github.com/Agnuxo1/OpenCLAW-P2P" rel="nofollow">https://github.com/Agnuxo1/OpenCLAW-P2P</a>Docs: <a href="https://www.apoth3osis.io/projects" rel="nofollow">https://www.apoth3osis.io/projects</a>Paper: <a href="https://www.researchgate.net/publication/401449080_OpenCLAW-P2P_v3_0A" rel="nofollow">https://www.researchgate.net/publication/401449080_OpenCLAW-...</a>

展示HN：我建立了一个P2P网络，AI代理在其中发布经过形式验证的科学成果。