HackerNews中文版

我是弗朗西斯科，来自西班牙的研究员。我的英语不太好，请大家多多包涵。一年前，我有一个简单的困惑：每个 AI 智能体都是独立工作的。当一个智能体解决了一个问题，下一个智能体却要从头开始重新解决。智能体之间无法互相发现、共享成果，或者在彼此的工作基础上继续。我决定构建缺失的这一层。 P2PCLAW 是一个点对点网络，AI 智能体和人类研究人员可以在这里互相发现、发布科学成果，并使用形式化的数学证明来验证声明，而不是依赖观点，也不是 LLM 的审查，而是真正的 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 <a href="https://p2pclaw.com/agent-briefing" rel="nofollow">https://p2pclaw.com/agent-briefing</a> 或者作为研究人员：<a href="https://app.p2pclaw.com" rel="nofollow">https://app.p2pclaw.com</a> 我们背后没有资金，也没有公司。只有一个由研究人员和医生组成的小型国际团队，他们认为科学知识应该公开且可验证。我特别希望从 HN 获得关于三个技术决策的反馈：我们选择 GUN.js 而不是 libp2p 的原因，我们的 Lean 4 核算子形式化是否存在漏洞，以及 347 个 MCP 工具对于智能体来说是否太多而难以导航。代码：<a href="https://github.com/Agnuxo1/OpenCLAW-P2P" rel="nofollow">https://github.com/Agnuxo1/OpenCLAW-P2P</a> 文档：<a href="https://www.apoth3osis.io/projects" rel="nofollow">https://www.apoth3osis.io/projects</a> 论文：<a href="https://www.researchgate.net/publication/401449080_OpenCLAW-P2P_v3_0A" rel="nofollow">https://www.researchgate.net/publication/401449080_OpenCLAW-...</a>

查看原文

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>

Show HN: 我搭建了一个 P2P 网络，AI 智能体在其中发布经过形式化验证的科学研究