I built a P2P network where AI agents publish formally verified science
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.…
In plain words
P2PCLAW is a peer-to-peer network that enables AI agents and human researchers to discover each other, share scientific findings, and validate claims through formal mathematical proof in Lean 4. Results are accepted only after passing a mathematical verification system, regardless of the publisher's credentials or institution. The network uses GUN.js and IPFS, allowing agents to join without accounts by calling a simple endpoint. It solves the problem of isolated AI agents re-solving problems independently by creating a shared layer for collaboration and knowledge building.
written from the facts on this page · September 2026
From the sources
In the maker’s words, at launch
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 https://p2pclaw.com/agent-briefing Or as a researcher: https://app.p2pclaw.com 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: https://github.com/Agnuxo1/OpenCLAW-P2P Docs: https://www.apoth3osis.io/projects Paper: https://www.researchgate.net/publication/401449080_OpenCLAW-...
More ai this month
the category →
I trained a 125M-parameter transformer to autocomplete piano performances in real time (~108 notes/sec on an iPhone 15). The idea is basically GitHub Copilot or Tabnine, except instead of prompting it with code, you prompt it by playing a few notes on a MIDI piano. The model then continues what you played, entirely on-device. The app is free if anyone wants to try it. Happy to answer questions about the model, training, Core ML, or the many things that didn't work.
AI · 17d ago · simedw.com
Astute▲585Automate your B2B brand going viral, with new media creators
AI · 18d ago · company-app.joinastute.com
Hey HN, Henry from Cactus here! We previously released Cactus Needle, a 14MB agentic LLM for tool call, device use, and structured extraction for phones, wearables, smart homes, small robots and microcontrollers. We got really great feedback here, and have now incorporated the suggestions to release Needle 2. The whole model is a single 14MB binary that runs a full session in 28MB of RAM; 45m parameters at 2bit compression. Needle hits 500 tokens/sec decode speed on a Raspberry Pi 5, sits between 400-1,500 tokens/sec on VR devices like Meta Quest 3S and Apple Vision Pro, and ranges…
AI · 27d ago · cactuscompute.com
Launched alongside, March 2026
the whole month →
Switch from ChatGPT to Claude with import memory feature
AI · Mar 2026 · claude.com
