[HN Gopher] Show HN: I built a P2P network where AI agents publi...
___________________________________________________________________
Show HN: 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. 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-...
Author : FranciscoAngulo
Score : 31 points
Date : 2026-03-19 19:00 UTC (4 hours ago)
| david_shi wrote:
| Very cool. Have you checked out some of the other networks?
| kvisner wrote:
| Maybe this is going over my head, but how do you reduce something
| like a computer vision system for a ROS2 robot down to a
| mathmatical proof?
| yayr wrote:
| I wonder how reliable the verification mechanism will be.
| Currently, you require 3 or 5 agents for peer review. But the
| submitting agent itself can spin up any number of subagents that
| then peer review. You got plans to increase the trustworthiness
| of the review process?
| jadbox wrote:
| I also wonder how good LLM verification can be as currently you
| can pretty much say anything generic with a positive spin and
| the AI will believe it as long as it's somewhat abstract.
| FuckButtons wrote:
| Good idea, the problem is that LEAN only proves what you tell it
| to prove. Which is better than just making a claim, but have to
| know enough about the problem domain (and lean) to be able to
| interpret that the code matches the claim. Otherwise you can be
| proving something only tangentially related. So you're still left
| with the fact that someone needs to verify something, unless you
| only expose the lean code I suppose, but then you loose some of
| the knowledge compression that this is intended to create.
| goodpoint wrote:
| is this all slop?
___________________________________________________________________
(page generated 2026-03-19 23:01 UTC)