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. ↓
The collaboration problem in mathematics is merge.
A crowd can produce more branches than one mind: lemmas, cases, examples, objections, counterexamples, searches, references. Polymath proved that. The cost arrived afterward. The branches had to become one proof, and the join still lived inside a moderator.
That was the ceiling. Conversation scaled. Trust stayed serial. A comment could be promising, but someone had to decide whether it fit the definitions, whether it duplicated another branch, whether its hidden premise was available, whether later work could safely stand on it.
Lean adds the missing operation. A proof assistant turns a contribution into an object with a statement, dependencies, and a checker. If the object is accepted, it joins the graph. The next contributor imports it and moves on. The project no longer re-trusts the contributor every time the lemma is used.
This is why Tao's turn toward Lean matters. He had already seen the ceiling. PFR was the controlled version: take a proof, expose the definitions and lemmas, mark the open obligations, let contributors work locally, and let the checker join the accepted pieces. Equational Theories was the large version: thousands of algebraic laws, millions of implications, human and automated search, one machine-checkable record.
The expert job moves to the cut.
Which intermediate object should exist? Which lemma is small enough for a stranger or a model to attack and strong enough for the graph to reuse? Which dependency blocks too much? Which library gap makes a paper-obvious step expensive? This is mathematical taste under a new constraint. The lead mathematician preserves the idea by choosing the pieces through which it can travel.
AI becomes useful inside that cut. A model can search a local region, propose a proof term, or hunt a counterexample. The checker decides whether the fragment joins. Weak generation becomes usable when the admission test is hard.
The boundary stays sharp. A proof assistant cannot supply the first abstraction. It cannot make every problem decomposable. It cannot tell a department how to reward the person who made the proof graph habitable. Proof objects may merge before credit does.
But the operation exists. That is the new fact. Tao did more than adopt a verification tool. He found a join operator for proof labor.
P.S. - Graph: extends math-is-becoming-engineering by moving from certification to mergeability; extends theorem-as-adoption-infrastructure by naming the upstream theorem-coordination object, where the proof graph coordinates the proof's own production; extends evaluation-bottleneck because the checker reduces one evaluation bottleneck while moving scarcity to decomposition and digestion; agrees with what-the-mathematicians-misunderstand on the separation of generation, certification, and digestion; shares mechanism with engineering-trust because trust attaches to the process that admits fragments into the graph.
Sources: Kevin Hartnett, "How Terry Tao Became an Evangelist for AI in Math," Quanta Magazine, June 8, 2026; Terence Tao, "Formalizing the proof of PFR in Lean4 using Blueprint," November 18, 2023; 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.