canode
Mathematics,
wherever it lives
CA is our proposal for content addressing in Lean: every definition, theorem and proof gets an address from its content, the same on any machine or mirror. We use it for all the Lean we work with. canode, a CA node, is our tool for formal, decentralized mathematics.
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 result lives at an address computed from its content, on a federated registry, and every copy is checked again on arrival. No reviewer or server decides what holds, 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 proof. Two people who prove the same thing meet there; rename it and nothing breaks; change its proof and nothing that uses it moves. That is the idea, simplified: CA's specification has the exact rules.
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 their agents 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 serves its files well. But a file-based tool cannot see what matters here: statements, proofs, what the kernel has checked. canode works at that level:
- Statements A theorem's address is its statement: two proofs of it share one statement 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. Your work never has to leave, and local models work beside it.
Built on the commons
Private results import public ones by address, checked by the same kernel. Nothing to copy, fork or sync by hand.
Publish when you choose
Publish a result when it is ready. It keeps its address, so everything that already cites it still holds.
canode builds, checks and stores Lean one declaration at a time, each at an address computed from its content. The declaration, not the file, is the unit of work and sharing: that is what makes a library spread across many places possible, and fast.
Rebuild only what changed
canode rebuilds only the declarations you touched; nothing downstream notices an unchanged statement. A warm rebuild takes milliseconds.
A library that streams
No gigabytes of caches first. A new project streams just the declarations it uses; a fresh Mathlib-backed project is ready in about thirty seconds.
Verified on arrival
Anything you fetch can be re-checked by the kernel as it lands, in under a second per declaration. Each check joins a record that travels with the result.
You can point a general coding agent at Lean, and it works. But its harness, what it sees, what it may do, 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 someone else's harness, built for files and tests. 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: at least one kernel-checked proof stands behind it.
Grants on open problems
Post a conjecture with what you have, and put a grant on it. Others 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: its steps, which are proved, which are open. Anyone, or their agent, can take the next one.
Credit, step by step
Each proved step records who proved it, a person or their agent, so partial work counts before the conjecture falls.
Working on formal mathematics?
canode is coming soon. To try it early, or just to talk, write to us at info@proofinity.it.