Yuri Not Igor

CSLib just launched — an open-source effort to formalize computer science in Lean, inspired by Mathlib. CS researchers, practitioners & enthusiasts are invited to get involved!

Learn more at:
🌐 cslib.io
🤝 Contribute: github.com/leanprover/c...

#LeanLang #LeanProver #CSLib #FormalVerification

Lean 4.28.0 is out! New symbolic simulation framework for 𝚐𝚛𝚒𝚗𝚍, user-defined 𝚐𝚛𝚒𝚗𝚍 attributes for custom tactics, a new 𝚜𝚘𝚕𝚟𝚎𝚛𝙼𝚘𝚍𝚎 in 𝚋𝚟_𝚍𝚎𝚌𝚒𝚍𝚎 for proof vs. counterexample search, and lean4checker available out of the box.

lean-lang.org/doc/referenc...

#LeanLang #LeanProver #ProofAssistant

Interesting, but what are we looking at specifically? An algebra for diagrams?

Real-time matters for humans co-editing docs.
For LLM agent workflows, robust async integration is usually the higher-leverage investment.

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.

AGENTS.md AGENTS.md is a simple, open format for guiding coding agents. Think of it as a README for agents.

Just to clarify: using your AGENTS.md, I meant

Orchestrate teams of Claude Code sessions - Claude Code Docs Coordinate multiple Claude Code instances working together as a team, with shared tasks, inter-agent messaging, and centralized management.

FWIW, I know it is not your goal, but it is quite easy to instruct Claude to use Agent Teams. See code.claude.com/docs/en/agen....

What if … Intrinsic HNSW?

The upper layers/universes are categorical realities where universe (n+1) is the sparse summary of the detailed concepts in (n).

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 …

The Year in Trump Cashing In In 2025, the President’s family has been making bank in myriad ways, many of which involve crypto and foreign money.

We don’t have a complete account of Donald Trump and his family’s finances. But a clear picture has emerged: enrichment of the First Family on a scale that is unprecedented in American history.
newyorkermag.visitlink.me/wKHd1v

If traditional computation is like building a house by first manufacturing every individual brick (intermediate data) and then laying them, fusion is like a 3D printer that creates the entire wall in one continuous motion, never needing the "intermediate" stage of loose bricks.

For someone new to all this, the generalization of a 1-category path using Batanin trees is quite fascinating—especially how one can derive source and target boundaries from any n-dimensional tree.

Lean for JavaScript Developers — overreacted Programming with proofs.

⚛️📝 New on Overreacted: Lean for JavaScript Developers

This chart captures well why I’m digging into Applied Category Theory (#ACT). Can we aim higher without being burned by a thousand cuts? Can we avoid throwing people-power at the problem just long enough to get acquired?

YouTube video by Pim de Haan Categories for AI 3: Categorical Dataflow: Optics and Lenses as data structures for backpropagation

Reviewing my understanding of monoidal categories from this great lecture: ‘Categories for AI: Categorical Dataflow’ by Bruno Gavranović www.youtube.com/watch?v=p4iR...
Highly recommended!

A blog post about the release is coming soon.

FYI: CatColab v0.3 is out (catcolab.org/help). Here are some of the highlights:

* Petri nets as a new logic
* Migrating models between different logics
* A functional rich text editor for text cells in notebooks
* Re-organized and significantly expanded docs (catcolab.org/help)

Fascinating how moving from 1-categories to 2-categories makes strictness optional.
But every equality you drop at one dimension has to be accounted for by new higher-dimensional equations (coherence laws) that ensure all the “up-to-isomorphism” structure still composes consistently.

Taking another careful read of “Cartesian Double Theories: A Double-Categorical Framework for Categorical Doctrines” by M. Lamberta and @epatters.bsky.social.

Time to raise the semantic level from 1D semantics, which give you models like sets with operations, to 2D semantics, which give you models like categories with structure.

I get a 404 ...

YouTube video by David Renshaw IMO 1996 P3: Lean 4 Formalization

IMO 1996 P3: Lean 4 formalization. ~ David Renshaw. youtu.be/5NbYtDfXfR4 #ITP #LeanProver #Math

What is really nice about the slice category alternative is that there is a recipe for creating deltas for any diagram, not just Set^SGr.

Alternatively, I could slice the functor category Set^SGr over G_BN, as Patterson, Lynch, and Fairbanks showed — by passing to slice categories, one can encode various categories of labelled data.

One approach I came across is to encode additions and removals as ZSets, then let the cumulative interpretation accumulate them. We could change the graph functor from G : SGr → Set to G : SGr → ZSet.

But what is the schema of each delta for a given time interval? Ideally, we should be able to systematically derive it from the snapshot schema.

Exploring an alternative to snapshot-based versioning: instead of capturing full snapshots at each point in time (as the paper describes), I’m proposing to record only the deltas—changes between successive states—and then use their cumulative interpretations to flexibly vary the time intervals.

Another very interesting paper directly in my area of interest is "Towards a Unified Theory of Time-Varying Data" (https://arxiv.org/pdf/2402.00206 ).

Shout-out to Sheaf Theory Through Examples by Daniel Rosiak. My studies over the past few weeks laid the groundwork, but this PDF was exactly what I needed at just the right moment.

https://arxiv.org/pdf/2012.08669