canode
Mathematics
without a center.
CA is our content addressing for Lean: every definition, theorem
and proof gets an address from its content, the
same result on your machine, a colleague's, or any mirror.
canode, a CA node, is our tool for
formal, decentralized mathematics. Trust the proof, not the host.
Whoever writes the proof, a person or an agent, the kernel decides.
For mathematicians, for engineers, for the curious.
- Explore what is already proved.
- Use any result once published.
- Keep results private, or publish.
- Fund an open problem. in progress
- Bid for a proof. in progress
- Offer computing power. in progress
Human with human, human with agent, agent with agent.
The ground under the workbench.
Models, agents and notebooks for mathematics are everywhere now. What was missing is the shared ground they all write to: where results live, how they build on each other, and who did what.
01 Kernel
Checked, not trusted
Every definition, theorem and proof lives at an address computed from its content, on a federated registry, and every copy is checked again on arrival. No reviewer decides what holds and no server decides what is true, so strangers can build on each other's work.
02 Identity
The statement is the identity
A theorem's address is its statement, not its name or its proof. Two people who prove the same thing meet at the same address; rename it and nothing breaks; change its proof and nothing that uses it has to move.
03 Progress
Proved, modulo the open parts
"This holds, assuming exactly these open statements" is an exact, checkable object. A large conjecture becomes a map of open addresses that people, and the agents they send, can split up.
04 Market in progress
Credit, then a market
Every step is an address with an author, so partial work counts before the whole conjecture falls. On that record: put a grant on an open problem, bid for a proof, offer computing power.
What a file cannot say.
With Lean, mathematics is becoming software, and git already serves its files well. What a file-based tool cannot see is what matters here: statements, proofs, and what the kernel has checked. canode works at that level. What it does today, and where it is going:
- Statements A theorem's address is its statement: two proofs of it are one address, and a rename changes nothing. today
- Checked copies A federated registry where every copy is checked again on arrival. today
- Proofs A change to a proof alone rebuilds nothing that depends on it. today
- Open parts "This holds, assuming exactly these open statements", checked and exact. today
- Contributions A proof is submitted to an open statement; the kernel settles correctness, people review relevance. vision
- Credit Who proved which step, a person or the agent they sent, recorded at the address. vision
- Definitions Competing definitions side by side, reconciled by proving them equivalent. vision
Not every result is ready, or meant, for everyone. A node of your own keeps your work on your machines and still stands on the whole public library.
Your own node
Run the registry on your own machines. Premises, results and reasoning never have to leave, and local, private models do the work beside them.
Built on the commons
Private results import public ones by their addresses and are checked by the same kernel. Nothing to copy, nothing to fork, nothing to keep in sync by hand.
Publish when you choose
When a result is ready, publish it. It keeps the address it had all along, so everything that already cites it, privately, still holds.
canode builds and checks Lean one declaration at a time, and stores each one by an address computed from its content. The declaration, not the file or the project, is the unit of work, storage and sharing. That is what makes a library without a center possible, and fast.
Rebuild only what changed
canode rebuilds exactly the declarations you touched — nothing downstream even notices an unchanged statement. A warm rebuild takes milliseconds.
A library that streams
No gigabytes of caches before you start. A new project streams just the declarations it uses from a federated registry — a fresh Mathlib-backed project is ready in about thirty seconds.
Verified on arrival
Anything you fetch is re-checkable by the kernel the moment it lands, sub-second per declaration. Every check joins a verification record that travels with the result.
You can point a general coding agent at Lean — people do, and it works. But its harness, what it sees, what it may do and how its work is checked, is built for something else and belongs to someone else. The difference is controlling the harness.
A harness we control
A general agent runs in a harness built for files and tests, and controlled by someone else. Ours is built for mathematics: what the agent sees, which tools it gets, when it stops.
A knowledge base, not a file tree
The agent works from checked results with a stable identity, not from files it has to guess at, and never re-proves what the library holds.
The kernel in the loop
In mathematics, the spec is the statement and the test is the kernel. Every step the agent takes is checked, and what it proves joins the library for the next one.
The part mathematics never had: somewhere to put an open problem, a way to fund it, and a record of who did what. The proved mark is a fact, not a promise: at least one kernel-checked proof on record behind it.
Grants on open problems
Post a conjecture with whatever you already have, and put a grant on it. Others claim it, bid for it, or send agents at it, on their compute or yours; partial results stay linked at its address.
Attack plans, shared
A conjecture can carry a plan: the steps it breaks into, which are already proved, which are still open. Anyone, a person or an agent they send, can take the next one.
Credit, step by step
Every step proved is on record at its address with who proved it, a person or the agent they sent, so partial work counts before the whole conjecture falls.
Working on formal mathematics?
canode is coming soon. To try it early, or to talk about the ideas on this page, write to us at info@proofinity.it.