I started optimizing for real-time distributed collaboration. After deep design work, I’m pivoting: JJ-style workflows fit LLM agents better. Agents work independently, then fetch/rebase/push. Lower complexity, clearer history, easier scaling.
Yuri Not Igor
@ydewit
- 7 Followers
- 69 Following
- 47 Posts
Real-time matters for humans co-editing docs.
For LLM agent workflows, robust async integration is usually the higher-leverage investment.
For LLM agent workflows, robust async integration is usually the higher-leverage investment.
The upper layers/universes are categorical realities where universe (n+1) is the sparse summary of the detailed concepts in (n).
What if … Intrinsic HNSW?
It is quite interesting that Hierarchical Navigable Small World (HNSW), a graph-based algorithm for high-dimensional nearest-neighbor search, seems isomorphic to the tower of universes in category theory …
Anne ApplebaumA "category" is a space of possibilities! Mathematically, it contains every possible object and every possible morphism". We don't compute or generate a category, unless it is somehow finitely presented, but we simply explore the paths within it.
Synthetic category theory ... a prescriptive substrate for computation in addition to a descriptive tool for formalization?
Olga PatlyukUkraine is blееding again.
Today Russia attacked Ternopil. 19 people diеd. 66 іnjured. 16 of them are children.
Please don’t stay silent.
Tell the world .
Sebastian UllrichAfter nine months of design, implementation, and orchestration, Lean's new module system I have been working on is now live in 4.26.0-rc1 and adopted throughout Mathlib. By introducing a system for checked and enforced API boundaries between files, it allows for changing proofs and other non-public information without any downstream rebuilds and drastically reduces the memory footprint of Mathlib imports to the lowest value ever since it was ported to Lean 4 two years ago.
