2024-01-01–ongoing
resources: 1634
tags: 199

This is a curated collection of browser bookmarks and YouTube videos I've gathered since 1st January 2024. Each resource is classified within a Wikipedia-inspired hierarchical tag system in an attempt to capture and organize my primary areas of interest.

The tag evolves continuously with the help of OpenAI's o3, which tends to its health and suggests refinements such as eliminating semantic duplicates, further subdividing nodes and ensuring that going down a level implies you've zoomed in on a narrower domain in a given field. This hopefully will help to keep the whole thing (hopefully) cohesive.

Quality varies semi-intentionally. There are many highly-qualitative resources but you'll also find more casual reads. This is because this is not a curated list in itself, the only moment of curation is me deciding this was good or interesting enough to bookmark.

To help with discoverability, you can find a fuzzy search bar. Each tag in tree also has a dedicated HTML page. Do note that some bookmarks are only tagged up to intermediate nodes!

Categories

Recent Bookmarks

The Cricket Language

Cricket is a lazy gradually-typed functional language with objects. It's very tiny but very expressive; anyone can implement it themselves!

An Introduction to Proofs with Dependent Types

This post introduces the basic ideas behind dependent-type-based proof assistants, and expressing logic with types and values.

A Beginner's Guide to Programming Language Academia

This post briefly maps out many different subfields of programming language theory, in an effort to make it more accessible to those outside academia.

Getting Started with Category Theory

Category theory is a beautiful and powerful field but it can feel impenetrable without the right entry point. This post hopes to serve as a sort of beginner's guide and reference.

Par Part 1: Sequent Calculus

Sequent Calculus is a way of doing logic that's very explicit and mechanical. It's used as an important system and notation for type theory and logic related to programming languages.

How does Lean work and what can it prove?

the quick and dirty of Lean

Time: Different from space

Over at Cosmic Variance, I learned that FQXi (the organization that paid for me to go to Iceland) sponsored an essay contest on “The Nature of Time”, and the submission deadline was las…

Lectures on Principles of Dependent Type Theory

This is a series of lectures aimed at graduate students on the modern design of full-spectrum dependent type theories, such as the core calculi of proof assistants like Agda, Coq, and Lean.

Custom Floating-Point Formats

This document describes the custom floating-point formats supported by the Tenstorrent Wormhole B0 architecture. These formats deviate from IEEE 754 standards in specific ways to optimize for AI workl

Subliminal Learning: Language Models Transmit Behavioral Traits via Hidden Signals in Data

Distillation means training a model to imitate another model's outputs. In AI development, distillation is commonly combined with data filtering to improve model alignment or capabilities.

See all bookmarks →

Recent Videos

What P vs NP is actually about

Explains the P vs NP problem by reducing arbitrary algorithms to SAT circuits, illustrating NP-completeness, reversibility, and implications for cryptography.

What Is an Interactive Theorem Prover? | Kevin Buzzard

Live demonstration of the Lean interactive theorem prover, showing how formal logic rules are encoded, manipulated, and verified, and discussing its role in mathematical research and future software tooling.

A Swift Introduction to Geometric Algebra

Provides a rapid, physics-motivated introduction to geometric algebra, covering multivectors, grades, geometric products, and rotors as an extension of linear-algebraic concepts.

A Brief Overview of Sheaf Theory - Part 1

The first lecture in a sheaf-theory series, defining presheaf stalks, sheafification, and exactness concepts such as kernels and images within a categorical framework.

Kan Academy: Introduction to Limits

An example-driven primer on categorical limits, building from sets and vector spaces to equalisers, fibre products, cones, and universal properties, aimed at newcomers to abstract category theory.

See all videos →