HashMath (Content-Addressed Formal Mathematics)

Here is the problem with formal math today. You write a proof in one system, I write the same proof in another, and they can't talk to each other. Every theorem, every proof, every definition answers to a name somebody had to choose, and names take coordination. What if every mathematical object identified itself, by what it actually says?

HashMath fixes this with one idea: content addressing. Instead of naming things, you hash them.

Content addressing#

Take a definition, serialize it to bytes, run it through SHA-256, and the hash is its identity. The same math always produces the same hash. No coordination needed. Two people on opposite sides of the world who write down the same definition have, automatically, agreed on its name.

So what exactly gets hashed? HashMath implements a full calculus of inductive constructions, the same type theory underneath Lean and Coq. You've got sorts, the types of types. You've got lambda abstractions and pi types, functions and their types. You've got applications, let bindings, and inductive types with their constructors and recursors. Every mathematical object in the system is a tree built from these constructors, and every tree has a hash.

De Bruijn indices#

One design choice is doing quiet, load-bearing work here. HashMath uses de Bruijn indices instead of variable names: the variable bound by the nearest lambda is zero, the next one out is one, and so on. So the term

λx. λy. x    becomes    λ. λ. 1
λa. λb. a    becomes    λ. λ. 1

Alpha-equivalent terms, terms that differ only in their variable names, are literally identical. No renaming, no ambiguity. Same structure, same hash.

Pause and try: write λx. λy. y x in de Bruijn notation. What happens to λa. λb. b a?

Inside the inner lambda, y is the nearest binder, so it is index 0, and x is one binder out, index 1. The term is λ. λ. 0 1.

And λa. λb. b a is λ. λ. 0 1 as well, the identical tree. That is the point: the names x, y, a, b were never part of the mathematics, so they are not part of the identity either. Both spellings get one hash.

The Merkle tree#

Hashing works like a Merkle tree. Every expression constructor gets a unique tag byte, one for lambda, one for application, one for sort, and so on. Then you hash the tag concatenated with the hashes of the children. For an application of a function f to an argument a:

hash(app f a) = SHA-256(TAG_APP || hash(f) || hash(a))

Hashes cascade up the tree: leaves first, then every node from the hashes of its children, until the root hash names the whole expression.

This gives you hash injectivity. Assuming SHA-256 is collision resistant, which is the standard cryptographic assumption, if two expressions hash to the same value, they are the same expression. Different tags for different constructors, fixed-size child hashes, unambiguous serialization: it all composes to give a global, unique identity for every mathematical object.

Pause and try: why does injectivity need the tag bytes and the fixed-size child hashes? What could go wrong without them?

Without tags, two different constructors with the same children would collide by construction, not because SHA-256 failed but because they were fed the same bytes. Distinct tags keep a lambda over a body and, say, a projection of the same body from ever serializing identically.

Without fixed-size child hashes, the byte boundaries inside the concatenation become ambiguous: one sequence of bytes could parse as several different lists of children. Fixed 32-byte hashes make the serialization parse one way only. Collision resistance only transfers to the trees if equal inputs to SHA-256 imply equal expressions, and that is exactly what the tags and the fixed widths guarantee.

A type checker, not a filing cabinet#

Hashing alone isn't enough. You need to know the math is correct. HashMath includes a full type checker for the calculus of inductive constructions: type inference, definitional equality with beta, delta, iota, and zeta reduction, universe polymorphism, inductive types with recursors, the whole stack. When you add a declaration to the environment, it gets type checked and then hashed. The hash is your receipt.

Real proofs are big; a single theorem might reference hundreds of sub-expressions. HashMath handles this with subterm hash-consing: any sub-expression larger than 33 bytes is replaced by a hash reference, and the sub-expression is stored separately, keyed by its own hash. If a thousand proofs all use natural numbers, the definition of nat is stored exactly once. Global deduplication, for free.

The network#

HashMath doesn't just store proofs locally. It distributes them over a peer-to-peer network using a Kademlia distributed hash table. You prove a theorem, hash it, and publish it to the network. Anyone can fetch it by hash, run the type checker themselves, and use it in their own proofs. No central authority. No gatekeepers. Permissionless formal mathematics.

The trusted computing base is small. You have to trust three things: the type checker, the SHA-256 implementation, and the serialization format. That's it. The parser, the elaborator, the network layer, the pretty printer: none of that affects soundness. If the type checker says a proof is valid and the hash matches, you can trust it, no matter where it came from.

The vision#

Imagine an ecosystem where AI systems generate thousands of proofs per hour. Naming conflicts can't happen, and nothing waits in a review queue. Identical statements and shared subterms deduplicate automatically, because the hashes match. Two agents who independently prove the same lemma generally get different hashes: the proof terms differ, and often even the statements do, n + m here, m + n there. The hash is honest about what identity means, syntactic, not semantic; equivalence is a theorem you prove, not a lookup. A growing, append-only library of verified mathematics, owned by no one, available to everyone.

HashMath says something simple: math is its own name. The content is the identity. There is no bureaucracy and no coordination, and nothing to trust but the checker. Just the math, its hash, and a network that remembers.

If you remember three things#

1. Content addressing replaces names with hashes: serialize an expression, SHA-256 it, and the hash is a global identity that needs no coordination, with de Bruijn indices making alpha-equivalent terms hash identically.
2. Merkle-style hashing with constructor tags and fixed-size child hashes makes the hash injective under collision resistance: same hash, same mathematics.
3. Soundness rests on a three-piece trusted base, the type checker, SHA-256, and the serialization, so proofs fetched from an untrusted peer-to-peer network are exactly as trustworthy as proofs you wrote yourself.