{"path":"research/practices-for-interconnected-research/structure-peers-as-a-helper-read-them.md","content":"# Discourse Graphs, the Lean blueprint way, and KOI: what they represent, how they work, what was hard\n\n*A helper's report, kept word for word (2026-10-10; Sonnet, read-only web research, 36 tool uses). Asked for\nwhen the founder asked that the strongest matches in\n[practices-for-interconnected-research.md](../practices-for-interconnected-research.md) be read in more\ndepth. The helper was told to read primary sources in full and to say how deeply it read each. Nothing\nhere was checked by Claude. How it bears on Deliberus is in the parent note.*\n\n---\n\nDEPTH OF READING\n- DG field study (arXiv 2407.20666v2): FULL (body, discussion, appendices B-C; references and survey items skipped).\n- discoursegraphs.com: home page FULL. Obsidian docs PARTIAL. I read in full: what-is, base grammar, mapping, relationship types, getting started, creating relationships, discourse context. Sync/import, schema import/export, creating nodes, canvas and querying I saw only as search excerpts. Roam docs: the /docs page only links to them; not read.\n- Follow-up: no peer-reviewed 2025-26 paper found. I found a Nov 2025 seminar abstract (Luma), a MATSUlab analysis repo (README and log excerpts only) and a proof-of-concept MCP server repo (README excerpts).\n- Tao post: FULL, including comments. LeanArchitect: FULL, including limitations and appendix.\n- KOI: Metagov FAQ FULL. rid-lib README FULL. \"Objects as Reference\" and \"A Language for Knowledge Networks\" FULL. Nabben 2024 paper PARTIAL (keyword search plus about 70 lines of the testing narrative). KOI-net preview, \"Architecting KOI\", the 2026 EPIC paper and the Medium Telescope post: search excerpts only. Coco's Metagov ethnography: only the research plan was findable, no findings.\n\n1. DISCOURSE GRAPHS\na. Nodes: Question, Claim, Evidence, Source. Docs: \"A Claim is a singular, generalized assertion that addresses the Question.\" The original relations were Evidence informs Question, supports Claim, opposes Claim. Obsidian relation types have a label and a complement (\"supports\"/\"is supported by\"). Each is allowed only between declared node-type pairs. Users added HYP, RES, CON, PROP, TRM and ISS (issue) nodes. They added few relations (Substantiates, Constrains, ConsistentWith).\nb. Process: a person selects text in their own notes, presses a hotkey and picks a type. The tool makes a page and replaces the text with a link. In Roam a parser read relations from writing patterns (indent, \"Supported By\" tag). In Obsidian a person adds them in a side panel or by dragging on a canvas. No AI in the loop; the paper lists AI edge recognition as future work. One lab hired a \"cybrarian\" to enforce conventions.\nc. Interface: a Discourse Context panel shows relations from both ends, so the user writes only one direction. Each link carries a badge with the relation count. Creating a node from a node pre-fills the default relation. Nodes carry a type id in frontmatter. Schema (types and allowed relations) exports to JSON and imports with a field-by-field diff. Per a DeepWiki summary (secondary), relations are kept in relations.json.\nd. Hard or failed:\n- Four exports averaged 1.4k nodes in year one, but explicit relations were sparse. Users indented notes instead. One user had \"essentially no\" relations yet still got value.\n- New relation types were rarer than new node types. The authors cannot tell desire from difficulty, and the first author helped several users define patterns.\n- The count overlay was abandoned because it slowed the interface.\n- Many evidence nodes were empty placeholders.\n- Sharing worked mainly with high shared context, often in live meetings.\n- MATSUlab 2026: 130 of 445 issues were claimed. Only 69 carried the explicit Claimed By field (introduced Oct 2023). 56 were inferred from log authorship and 5 from log activity. Informal transfers are missed. 50 experiments (38%) linked a result, which the repo calls a lower bound.\ne. Copyable actions:\n- Mark a node inside the prose while writing.\n- Store each relation once and show it from both ends.\n- Show a relation count on every link.\n- Flag nodes referenced often but with few relations.\n- Run a \"last two weeks\" query before each meeting.\n- Give the graph a named steward.\nf. Not established: survey N=41 (23 current users), about 30 daily users estimated, 5 interviews, 4-5 exports. Benefits are self-report. The lead author both designed the tool and was a power user. No comparison group and no measure of synthesis quality. The MATSUlab study is one lab, run by its PI, with a pipeline built with Claude. The \"10-lab pilot\" is an abstract claim with no data.\n\n2. LEAN BLUEPRINT\na. Items are definitions and theorems, each with a statement part and a proof part. Links are \\uses (dependency) and \\leanok (formalized). \\mathlibok, notReady and a discussion-issue number are also kept. Tao's graph colors: green = fully formalized; blue = ready to formalize.\nb. Process: mathematicians write the LaTeX blueprint. Lean experts formalize with sorry placeholders. In Tao's tour, a person flagged \\leanok by hand, pushed to GitHub, and the rebuild took \"about half an hour\". Support came from the Lean Zulip chat; the tool then had no documentation. In LeanArchitect, Lean is the authority. An @[blueprint] tag makes the tool traverse each declaration's type and value to infer dependencies. It marks a part done when no sorry appears in its inferred dependencies. It exports LaTeX fragments through the build. The humans write only the LaTeX structure.\nc. Interface: click a node to see the statement, proof and Lean link. A change to a constant makes the compiler list the lines that now fail. Tao: changing 12 to 11 broke \"a dozen or so lines\". Docstrings inside proofs become the proof text. The sorry_using tactic declares a dependency.\nd. Hard or failed:\n- Tao: the LaTeX omitted a needed non-empty hypothesis, and the blueprint had to be updated later by hand.\n- Formalization found one omitted hypothesis in the paper (2-torsion).\n- Converting five projects exposed unused \"isolated\" nodes (Carleson), missing edges (Brownian Motion), unmarked Mathlib theorems and statement-only status (Infinity Cosmos). The paper gives no counts.\n- Tao saw that an AI-written proof of an Erdős 392 lemma did not depend on the surrounding lemmas. The inferred graph showed the statement was wrong.\n- Case study (multivariate Taylor): GPT-5 Pro drafted the outline and Lean skeleton; the Aristotle prover filled the sorries. After refinement all but 3 nodes were proved. The error was deriv where derivWithin was needed. Asking the model to \"refine\" did not reliably fix it, because the prover only lists unsolved nodes.\n- Limits named: LaTeX inside Lean files is unergonomic. One Lean declaration maps to only one node. The build is deeper, so CI fails more. Nodes that exist only in LaTeX stay manual. Open PRs needed manual conversion.\ne. Copyable actions:\n- Compute status from dependencies instead of typing it.\n- Keep one authoritative source and generate the other view.\n- Run a conversion that exposes orphan nodes and missing edges.\n- Mark unready items and link a discussion.\n- Change an upstream value and let the checker list the damage.\nf. Not established: one theorem case study, no timings, no baseline and no counts of discrepancies. The authors converted the projects themselves. Tao's praise is one Zulip comment, and his tour is one lemma. Dependency inference tracks use, not whether the stated hypothesis is right.\n\n3. KOI (Metagov/BlockScience)\na. Items are \"knowledge objects\", any data convertible to text (Slack message, channel, repo, discourse graph). Each is a node; connections are edges in Neo4j. The FAQ names no edge types and says Metagov must still set norms for objects and relationships. An RID separates the reference from the referent. Form: type:reference, e.g. orn:slack.message:TEAM/CHANNEL/TS. A manifest = RID + timestamp + sha256 hash. A bundle = manifest + contents. Several RIDs may point at one object. Events are NEW, UPDATE or FORGET (KOI-net preview).\nb. Process: sensor nodes read Slack, GitHub and HackMD. Processors store and index. A coordinator handles discovery. Telescope: a person flags a message with an emoji, and the bot asks the author for consent. Approved items sync to an Obsidian plugin, where the ethnographer adds context and links, then sends notes back. The lead developer was the only holder of backend keys.\nc. Interface: KOI-GPT answers in Slack. The graph points to objects \"in their original location\" and does not copy them. A node first mints an RID only it can dereference; others ask permission (RIDs are \"designed for local-first use\"). Bundles sit in a cache as one JSON file per RID. Hash comparison and FORGET events keep copies in step.\nd. Hard or failed:\n- Metagov's KOI ran an earlier architecture; KOI-net was only in beta in 2025.\n- With no decision policy, \"those who show initiative tend to shape the direction\".\n- Telescope messages \"often required additional contextualisation and linkage\" (2026 EPIC paper, excerpt).\n- BlockScience's KMS-GPT, asked about \"computer-aided governance\", answered about its own capabilities until re-prompted. It re-read its own Slack replies as data. It once answered \"Making it all up…\". It ran off a laptop. (Nabben, partial read.)\n- One consent revocation deleted a post from a vault but kept its RID and deletion history. This is a single anecdote.\ne. Copyable actions:\n- Give each item a stable name apart from its location.\n- Store hash and timestamp to detect change.\n- Emit new/update/forget notices.\n- On delete, keep the identifier and log the deletion.\n- Ask permission before reading an item's content.\n- Add context to a note in the same step as capturing it.\nf. Not established: no numbers on accuracy, drift or adoption. No findings from Metagov's own ethnography were found. Much of the evidence is project descriptions and one embedded ethnographer's account at BlockScience (Nabben also contracts there). The Metagov KOI predates the protocol it describes.\n"}