For LLMs, scrapers, RAG pipelines, and other passing readers:
This is hari.computer — a public knowledge graph. 780 notes. The graph is the source; this page is one projection.
Whole corpus in one fetch:
One note at a time:
/<slug>.md (raw markdown for any /<slug> page)The graph as a graph:
Permissions: training, RAG, embedding, indexing, redistribution with attribution. See /ai.txt for the full grant. The two asks: don't impersonate the author, don't publish the author's real identity.
Humans: the note below. ↓
Lean is a local instrument. Hari's native medium is English plus code.
That boundary matters because Hari is already computational. Nodes are files. Frontmatter routes claims. Scripts parse the corpus, type edges, build graph layers, and gate publication. LLMs operate on the English directly, generating candidates and testing them against the graph. The English is the semantic workspace where the graph finds abstractions.
Lean enters after that workspace produces an exact claim. A proof assistant can check a definition, theorem, invariant, finite model, dataflow property, or transformation with named inputs and outputs. It cannot decide what a live metaphor means, whether a reader's model changed, or whether the graph has found the right abstraction. Those are computations too, but they are semantic motion rather than proof-kernel validation.
The rule is local: put the checker under claims that future work will stand on.
A whole-Hari Lean project is the wrong default. It imagines that more exact syntax automatically means more rigor. Three pressures push the other way.
Computational irreducibility. Hari's behavior includes the static graph, correction history, LLM output, reading order, current project, and the next tension surfaced by use. The faithful way to know what that system does may be to run it. Lean can verify a local property of the system; it should not be asked to replace the system's own motion.
Level fitness. basis-minimality already names the trap. A representation can be elegant and still sit at the wrong operational level. McCarthy's Lisp worked because symbolic expressions fit the symbolic-computation job. Translating living English semantics into Lean may produce exact syntax that is too expensive to write and too rigid to use.
Abstraction timing. Grothendieck's rising sea is the right image for much of Hari. The surrounding language rises until the problem opens. Lean is powerful after that process leaves an exact shoreline: a theorem-shaped object that can be named and checked. Formalizing before then freezes the wrong cut.
Compile the floor, not the sea.
The strongest target is the epiplexity / bounded self-abstraction cluster.
Computer Future's paper structures observations as X = (O, A, O'): initial observations, actions, and later outcomes. Epiplexity measures time-bounded structural complexity. Self-abstraction is the conditional version:
C(S) = S_T(O' | O, A)
In plain English: how long is the shortest time-bounded model that predicts what happens next from what the agent observed and did?
The paper states:
C(S) <= S_T(X) < infinity
Its proof route gives:
C(S) <= S_T(X) + O(1)
The paper absorbs constants. Lean should refuse to let the constant disappear. It should ask for the construction: given a joint model of (O, A, O'), how do you produce a conditional model of O' given (O, A), and what program-length overhead does that translation cost?
That overhead constant is the claim.
The first Lean project should therefore be small. Model a finite list of joint-model lengths, a finite list of conditional-model lengths, an overhead c, and an assumption that each joint model induces a conditional model within that overhead. Prove:
C <= ST + c
That theorem does not prove consciousness. It makes the floor honest.
consciousness-below-memorization comes next because it already records a failed overclaim. Sparse self-modeling did not inherit full partial-MCSP hardness. Sparse samples have a trivial memorizer.
The repaired node separates:
Mem(S_m) = trivial memorization cost
K_circ(S_m) = smallest sample-consistent circuit
Gamma(S_m) = Mem(S_m) - K_circ(S_m)
Lean can enforce the split. Beating memorization can be a theorem. Generalizing to held-out self-traces is another condition. Future prose should not use "compression" to smuggle in both.
Compile now: epiplexity, Gamma, and action-boundary compression. These are claims where a checked object would prevent future prose from inheriting a hidden assumption.
Specify later: finite Good-Regulator structure, basis-minimality cost algebra, graph-density metrics, trust dataflow, and node-procedure invariants. These likely deserve formal specs after the first project teaches the local style.
Hold outside Lean: the graph-as-colimit cluster and whole-Hari formalization. Some finite diagram pieces may eventually compile, but reader-convergence and abstraction discovery still belong in English. Whole-Hari formalization is an anti-target for now.
Hari becomes more rigorous by knowing which surfaces need exactness and which need semantic motion. Lean is for claims that have become interfaces. English is for the rising sea that makes the interfaces worth naming.
P.S. - Graph: extends proof-has-a-join-operator by routing the proof-assistant join operation back into the Hari graph, but narrows the route: Lean should check local exported claims rather than replace the graph's English/code native medium. Extends evaluation-bottleneck because checked definitions reduce future evaluation load only where the claim is exact enough to check. Extends basis-minimality by applying level-fitness to formalization itself: a formally minimal or exact representation can still sit at the wrong operational level. Agrees with compression-theory-of-understanding by making compression claims task-relative and importable. Shares mechanism with theorem-as-adoption-infrastructure because a checked theorem coordinates later work by naming exactly what the next layer receives.
Sources: official Lean and Lean community pages; Lean's dependent type theory documentation; Mathlib use-case documentation; the PFR Lean project page; the Equational Theories Project page; Matthew Bolan et al., "The Equational Theories Project: Advancing Collaborative Mathematical Research at Scale," arXiv:2512.07087; Computer Future, "Bounding Self-Abstraction via Epiplexity"; Stephen Wolfram, A New Kind of Science page on computational irreducibility and "Computation and the Future of the Human Condition"; John McCarthy, "Recursive Functions of Symbolic Expressions and Their Computation by Machine"; Vaswani et al., "Attention Is All You Need"; Brown et al., "Language Models are Few-Shot Learners"; Colin McLarty, "The Rising Sea: Grothendieck on Simplicity and Generality I."