A Universe of Sorts
Siddharth Bhat
 Stuff I learnt in 2022
 You don't know jack about data races
 Training a custom model for Lean4
 Stratified synthetsis
 Libtpu
 Mutual recursion elaboration in Lean
 Subject reduction in Lean
 Big list of GNU Binutils
 Automatically building a JIT compiler
 Model theory
 Mathematical logic: real closed fields
 Sturm's theorem
 CMake
configure_file
 List symbols in a file
 Axiom K versus UIP
 Linear vs uniqueness types
 Better shell history with atuin
 Better git diff with delta
 Any model of lean must have all inductives
 Index over the past, fiber over the future
 Kripke style logical relations (TODO)
 Impredicativity
 Type formers need not be injective
 There cannot be a type of size the universe:
 The dependently typed expression problem
 Rotation distance as a metric on binary trees
 Motivation for modal logic
 Scones
 Presheaf models of type theory
 Weighted limits via collages
 Disjoint Coproduct
 Universal coproduct / stable under pullback
 Leibniz Equality in Lean4
 Strong normalization of STLC
 Subobject classifiers of $N \to FinSet$, or precosheaf of $FinSet$
 Dimensions versus units
 HoTTesT: Identity types
 Philosophy of History
 Left and right adjoints to inverse image [TODO ]
 Paredit via adjoints
 Less than versus Less than or equals over Z
 Allegories and Categories
 Partial function as span
 Post's Problem [WIP ]
 Turing degree
 Ultraproducts in Logic [WIP ]
 Pivot tables are indexed categories [WIP ]
 Kleene Tree [WIP ]
 Compactness theorem as compactness of stone spaces [WIP ]
 Setting up windows box on google cloud
 Proof that there is a TM whose halting is independent of ZFC
 Contradiction from nonpositive occurence
 The constructible universe L
 Scrivano for note taking
 Godel completeness theorem
 Uniform proofs, focused proofs, polarization, logic programming
 Why cut elimination?
 Forcing to add a function
 Diaconescu's theorem
 Forcing machinery
 Partial Evaluation, Chapter 3
 Partial Evaluation, Chapter 1
 Diagonal lemma for monotone functions
 Cantor Schroder Bernstein via fixpoint
 Maximal Ideals of Boolean Algebras are Truth Values
 Crash course on DCPO: formalizing lambda calculus
 Resolution algorithm for propositional logic
 Completeness for first order logic
 Compactness theorem of first order logic
 WIP: Tarski's undefinability theorem
 WIP: Conservative extension to type theory
 First order logic: Semantics
 full abstraction in semantics (TODO)
 You could have invented Sequents
 Fibrational category theory, sec 1.1, sec 1.2
 Simple Type Theory via Fibrations
 Realisability models
 Naming left closed, right open with start/stop
 Nested vs mutual inductive types:
 MiniSketch [TODO ]
 Finger trees data structure [TODO ]
 HAMT data structure [TODO ]
 Embedding HOL in Lean
 Module system for separate compilation
 Second order arithmetic
 Lean4 Dev Meeting
 Categorical model of dependent types
 How should relative changes be measured
 Logic of bunched implications
 Coends
 Natural Transformations as ends
 Ends and diagonals
 Parabolic dynamics and renormalization
 Quantifiers as adjoints
 TLDP pages for bash conditionals
 Remainder, Modulo
 Parameters cannot be changed anywhere , not just in return location
 LCNF
 Predicative v/s Impredicative: On Universes in Type Theory
 Testing infra in Lean4
 Autocompletion in Lean4
 Inductive types
 Parameter verus Index
 HNF versus WHNF
 Different types of arguments in Lean4:
 Big list of lean tactics
 Hyperdoctrine
 Fungrim
 Category where coproducts of computable things is not computable
 Homotopy continuation
 Relationship between linearity and contradiction
 Monads from Riehl
 Combinatorial Cauchy Schwarz
 Bezout's theorem
 Example for invariant theory
 Counterexample to fundamental theorem of calculus?
 Why a sentinel of
1
is sensible  Data structure to maintain mex
 Scatted algebraic number theory ideas: Ramification
 Coreflection
 Better
man
Pages via info
 The Zen of juggling three balls
 Example of lattice that is not distributive
 Patat
 Common Lisp LOOP Macro
 MitchellBénabou language
 Hyperdoctrine
 Why is product in Rel not cartesian product?

simp
in Lean4  Big list of Lean4 TODOS

unsafePerformIO
in Lean4:  Big List of Lean4 FAQ
 Sheaves in geometry and logic 1.2: Pullbacks
 Sheaves in geometry and logic 1.3: Characteristic functions of subobjects
 Common Lisp Debugging: Clouseau
 Drawabox: Lines
 Common Lisp Beauty: paths
 Logical Predicates (OPLSS '12)
 Logical Relations (Sterling)
 Pointless topology: Frames
 Introduction to substructural logics: Ch1
 Integrating against ultrafilers
 wegli: Neat tool for semantically grepping C++
 Mostowski Collapse
 Spaces that have same homotopy groups but not the same homotopy type
 Fundamental group functor does not preserve epis
 Epi in topological spaces
 Permutation models
 Almost universal class
 Godel operations
 Orthogonal Factorization Systems
 Orthogonal morphisms
 Locally Presentable Category
 Remez Algorithm
 Permission bits reference
 Papers on Computational Group Theory
 Kan Extensions: Key idea
 Interleaved dataflow analysis and rewriting
 Central variable as
focal
 Wilson's theorem
 General enough special cases
 XOR and AND relationship
 Geometry of complex integrals
 Green's functions
 CP trick: writing exact counting as counting less than
 CP trick: Heavy Light Decomposition euler tour tree
 Counting with repetitions via pure binomial coefficients
 Fundamental theorem of homological algebra [TODO ]
 Projective modules in terms of universal property
 How ideals recover factorization [TODO ]
 Centroid of a tree
 Path query to subtree query
 Pavel: bridges, articulation points for UNDIRECTED graphs
 Segtree: range update, point query [TODO ]
 Monadic functor
 Injective module
 Proof that $Spec(R)$ is a sheaf [TODO ]
 Projections onto convex sets
 LM algorithm for nonlinear least squares
 Backward dataflow and continuations
 Coordinate compression with
set
and vector
 Hilbert polynomial and dimension
 Cost of looping over all multiples of $i$ for $i$ in $1$ to $N$
 Stuff I learnt in 2021
 Cayley hamilton for 2x2 matrices in sage via AG
 LispWorks config
 Birkhoff Von Neumann theorem
 Latin Square
 Assignment Problem
 Interpolating homotopies
 Example where MIP shows extra power over IP
 Lazy reversible computation?
 Theorem coverage as an analogue to code coverage
 Lazy GPU programming
 Projections onto convex sets [TODO ]
 BGFS algorithm for unconstrained nonlinear optimization [TODO ]
 LM algorithm for nonlinear least squares [TODO ]
 Backward dataflow and continuations
 The tyranny of structurelessness
 Simple Sabotage Field Manual
 Counting permutations with #MAXSAT
 Coloring
cat
output with supercat
 Reader monoid needs a hopf algebra?! [TODO ]
 Monads mnemonic
 Card stacking
 Representation theory for particle physics [TODO ]
 SSH into google cloud
 Comma & Semicolon in index notation
 Spin groups
 How to write in biblical style?
 Undefined behaviour is like compactification [TODO ]
 God of areppo
 Classification of lie algebras, dynkin diagrams
 Weird free group construction from adjoint functor theorem
 bashupload
 When are the catalan numbers odd
 Discrete probability [TODO ]
 Geodesic equation, Extrinsic
 Connections, take 2
 Dropping into tty on manjaro/GRUB
 Why the zero set of a continuous function must be a closed set
 Derivatives in diffgeo
 Building stuff with Docker
 Lie derivative versus covariant derivative
 The Tor functor
 Sum of quadratic errors
 HipHop and Shakespeare
 Write thin to write well
 Hidden symmetries of alg varieties

fd
for find
 Thu Morse sequence for sharing
 Elementary and power sum symmetric polynomials
 Projective spaces and grassmanians in AG
 Mnemonic for why
eta
is unit:  Fundamental theorem of galois theory
 Counterintuitive linearity of expectation [TODO ]
 Metis
 Tooling for performance benchmarking
 Normal field extensions
 Eisenstein Theorem for checking irreducibility
 Gauss Lemma for polynomials
 How GHC does typeclass resolution
 Defining continuity covariantly
 Why commutator is important for QM
 Deriving pratt parsing by analyzing recursive descent [TODO ]
 Level set of a continuous function must be closed
 HPNDUF  Hard problems need design up front!
 Separable Extension is contained in Galois extension
 Primitive element theorem
 Separable extension via embeddings into alg. closure
 Separable extensions via derivation
 Irreducible polynomial over a field divides any polynomial with common root
 Galois extension
 Separability of field extension as diagonalizability
 Motivation for the compactopen topology
 Example of covariance zero, and yet "correlated"
 Hypothesis Testing
 Dumb mnemonic for remembering adjunction turnstile
 Delta debugging
 Tidy Data
 Normal subgroups through the lens of actions
 Writing rebuttals, Tobias style
 LCS DP: The speedup is from filtration
 Poisson distribution
 F1 or Fun : The field with one element
 McKay's proof of Cauchy's theorem for groups [TODO ]
 Odds versus probability [TODO ]
 ncdu for disk space measurement
 nmon versus htop
 Schrier sims  why purify generators times coset
 Vyn's feeling about symmetry
 Convergence in distribution is very weak
 Class equation, Pgroup structure
 Sylow Theorem 1
 Fuzzing book
 Filtered Colimits [TODO ]
 Fisher Yates
 Bucchberger algorithm
 GAP permutation syntax
 Why division algorithm with multiple variables go bad
 Integral elements of a ring form a ring [TODO ]
 "Cheap" proof of euler characteristic
 Siefert Algorithm [TODO ]
 Cap product [TODO ]
 Cup product [TODO ]
 Colimits examples with small diagram categories
 Limits examples with small diagram categories
 Classification of compact 2manifolds [TODO ]
 Gauss, normals, fundamental forms [TODO ]
 Second fundamental form
 Shape operator [TODO ]
 Theorem Egregium / Gauss's theorem (Integrating curvature in 2D) [TODO ]
 Integrating Curvature in 1D [TODO ]
 Fundamental theorem of symmetric polynomials
 DP over submasks
 Dual of Planar Euler graph is bipartite
 Yoneda preserves limits
 Separable Polynomials and extensions
 Limits of a functor category are computed pointwise.

a + b = (a or b) + (a and b)
 Intuition for why choosing closedclosed intervals of
[1..n]
is $(n+1)C2$  Thoughtful discussion on the limits of safe spaces
 Semidirect product: Panning and Zooming
 Longest Convex Subsequence DP
 Representation theory of $SU(2)$ [TODO ]
 Why quaternions work better
 DFA to CFG via colimits?
 Why pointless topology is powerful
 Denotational semantics in a few sentences
 Monge Matrix
 Fixpoint as decorator
 Combinatorial generation algorithms
 Perform DP on measures, not indexes.
 Alternative version of MyhillNerode
 Polya Enumeration
 Weighted Burnside Lemma
 Cycle index polynomial
 Mnemonics For Symmetric Polynomials
 Uses of minimal string rotation
 Suffix Automata
 Simpson's Paradox
 Myhill Nerode Theorem
 Linearity of expectation for sampling
 Dedekind MacNiellie
 Good and bad combinatorics: intro to counting
 Expected number of turns to generate all numbers
1..N
(TODO)  Diameter in single DFS (TODO)
 Min cost flow (TODO)
 Clojure: minimal makefile for REPL driven dev with Neovim
 Delimited continuations
 Never forget monic again
 Weird canonical example of monic and epic: left/right shift
 Playing guitar: being okay with incorrect chords
 Sparse table
 Duval's algorithm
 Amortized complexity from the verifier perspective
 Relationship betwee permutations and runs
 Brouwer's fixed point theorem
 XOR on binary trie
 Inconvergent: beautiful generative art
 Prefix/Border function
 Shortest walk versus shortest path
 Minimal tech stack
 FFT
 codeforces rating of some GMs
 Continuum TTRPG
 Words to know in target language
 DP on subarrays
 Vis editor cheat sheet
 Mean, Median and Jensen's
 The similarity between labellings and representations
 L1 norm is greater than or equal to L2 norm
 Z algorithm
 For a given recurrence, what base cases do I need to implement?
 Number of distinct numbers in a partition
 Splitting $f(x) = y$ into indicators
 Why searching for divisors upto
sqrt(n)
works  Heuristics for the prime number theorem
 Sum of absolute differences of an array
 GCD is at most difference of numbers
 implementing GCD and LCM
 Centroid of a tree
 Center of a tree
 Image unshredding as hamiltonian path
 Distance between lines in nD

lower_bound
binary search with closed intervals  Sliding window implementation style
 Kawaii implementation of
x = min(x, y)
 CSES: Counting Towers
 Smallest positive natural which can't be represented as sum of any subset of a set of naturals
 Example of RVs that are pairwise but not 3way independent.
 Notes on Liam O Connor's thesis: Cogent
 C++
lower_bound
, upper_bound
API  Books that impart mental models
 Subarrays ~= prefixes
 Operations with modular fractions
 Modular inverse calculation
 The number of pairs
(a,b)
such that ab≤x
is O(xlogx)
 DP as path independence
 Binary search to find rightmost index which does not possess some property
 Correctness of
lower_bound
search with halfopen intervals  Greedy Coin change: proof by probing
 Clean way to write burnside lemma
 The groupoid interpretation of type theory
 Mnemonics for free = left adjoint
 Where to scratch a cat
 Mnemonic for Specht module actions
 Quotes from 'Braiding Sweetgrass'
 Transfinite recursion: Proof
 Transfinite induction: Proof
 Thoughts on playing EmBm
 An explanation for why permutations and linear orders are not naturally isomorphic
 We can't define choice for finite sets in Haskell!
 Geomean is scale independent
 Thoughts on playing Em Bm.
 Induction on natural numbers cannot be derived from other axioms
 Ordinals and cardinals
 Musing about Specht modules
 Every continuous function on $[a, b]$ attains a maximum
 Invisible cities
 Associativity of addition in cubicaltt
 Etymology of fiber bundle $F \rightarrow E \rightarrow B$
 Galois correspondence, functorially
 CubicalTT: sharpening thinking about indexed functions
 Functors to motivate adjuntions
 Madoka Magica: plot thoughts
 Chain rule functorially
 Lagrange multipliers by algebra
 Specht module construction
 Even and odd functions through representation theory
 Greg egan: Orthogonal
 Simplicial approximation: maps can be approximated by simplicial maps (TODO)
 Excision (TODO)
 Marshall: Andrej (TODO)
 Limit is right adjoint to diagonal
 Working out why right adjoints preserve limits.
 Limit/Colimit/Cone/Cocone: the arrows are consistent!
 Representable Functors
 Why terminal object is a limit
 Excluded middle is not false in intuitionistic logic
 Yoneda Lemma and embedding
 GHCID
 Character theory
 Cofibration
 Emily Riehl Contrability as uniqueness
 Cofactor as derivative of determinant
 Homology, the big picture
 Normaliztion by evaluation (TODO)
 Legal Systems very different from ours
 Lefschetz fixed point theorem (TODO)
 Shrinking wedge of circles / Hawaiian earring (TODO)
 Simplicial approxmation of maps (TODO)
 Lebesgue number lemma (TODO)
 Lean internals Cheat Sheet
 MicroUI
 Proof of tree having (V1) edges
 Creating PDFs to read code
 Bias and gain
 Barycentric subdivision: edge length decreases
 Homotopic maps produce same singular homology: Intuition
 Singular homology: induced homomorphism
 Demoscene tools
 Binaural Beat
 Low pass filter by delaying
 Octaves are double frequency apart (TODO)
 Bias and gain
 Show, don't tell
 Try and think of natural transformations as intertwinings
 Subobject classifier measures how much we need to pay to access fact
 Spectral norm of Hermitian matrix equals largest eigenvalue (TODO)
 Penrose cohomology [TODO ]
 Bicycle wheel proof of Gauss Bonnet (TODO)
 What is Levi Cevita trying to describe (TODO)
 Torsion as giving monodromy of path lifts (TODO)
 Cartan's spiral staircase (TODO)
 Weingarten map
 When maps cannot be lifted to the universal cover
 Nets from Munkres (TODO)
 Limit point compactness from Munkres
 Proof of Heine Borel from Munkres (compact iff closed, bounded)
 Alexandrov topology
 Zeroth singular homology group: Intuition
 Examples of fiber products / pullbacks
 Covariant derivative
 Clackety sounds:
bucklespring
 Submersions and immersions
 Ehrsmann connection
 Quotes from the culture
 Lie bracket commutator as infinitesimal conjugation
 Thoughts on proof of fundamental group of unit circle
 Pasting lemma
 Tensoring with base ring has no effect
 Seeing the semidirect product of the dihedral group.
 Animating rotations with quaternion curves
 Mnemonic for homtensor and leftright adjoints
 Construction of tensor product: Atiyah macdonald
 Recovering topology from sheaf of functions: Proof from Atiyah Macdonald
 Urhyson's lemma
 Compact Hausdorff spaces are normal
 Stone representation theorem: Proof from Atiyah Macdonald
 Covariant Hom is left exact
 Internal versus External semidirect products
 Splitting of semidirect products in terms of projections
 Tensor is right exact
 Semidirect product as commuting conditions
 Exact sequences for semidirect products; fiber bundles
 Semidirect product is equivalent to splitting of exact sequence
 Intro to topological quantum field theory
 Non examples of algebraic varieties
 Nilradical is intersection of all prime ideals
 Exactness of modules is local
 Quotient by maximal ideal gives a field
 Ring of power series with infinite positive and negative terms
 Mean value theorem and Taylor's theorem. (TODO)
 Cayley Hamilton
 Nakayama's lemma
 Vector fields over the 2 sphere
 Learning to talk with your hands
 Lovecraftisms
 Hairy ball theorem from Sperner's Lemma (TODO)
 CS and type theory: Talks by vovodesky
 Hilbert basis theorem for polynomial rings over fields (TODO)
 Covering spaces
 Wedge Sum and Smash Product
 Quotient topology
 CW Complexes and HEP
 Stable homotopy theory
 Simply connected spaces
 Finitely generated as vector space v/s algebra:
 Weak and Strong Nullstllensatz
 Screen recording for kakoune pull request
 Intuition for why finitely presented abelian groups are isomorphic to product of cyclics
 Euler characteristic of sphere
 John Conway: The symmetries of things
 Semidirect product mnemonic
 Non orthogonal projections
 Why did maxwell choose his EM wave to be light?
 Fast string concatenation in python3
 Split infinitive
 Yoneda from string concatenation
 Right Kan extensions as extending the domain of a functor
 Non standard inner products and unitarity of representations
 take at most 4 letters from 15 letters.
 Flat functions
 Hopf Algebras and combinatorics
 Butcher group
 Neovim frontends
 A semidirect product worked on in great detail
 Direct and Inverse limits
 LEAN 4 overfrom from LEAN together 2021
 BLM master thesis
 Hololive subculture
 RSK correspondence for permutations
 Djikstra's using a segtree
 Markov and chebyshev from a measure theoretic lens
 Among any 51 integers, that are 2 with squares having equal value modulo 100
 $1^n + 2^n + \dots + (n1)^n$ is divisible by $n$ for odd $n$
 $10^{3n+1}$ cannot be written as sum of two cubes
 Coqclub: the meaning of a specification
 SQLite opening
 Old school fonts
 Stalking
syzigies
on hackernews  Conditional probability is neither causal nor temporal
 Hook length formula
 The tyranny of light
 Muirhead's inequality
 Rearrangement inequality
 Triangle inequality
 The Heather subculture
 Frobenius Kernel
 Galois theory by "Abel's theorem in problems and solutions"
 Galois theory perspective of the quadratic equation
 Burnside lemma by representation theory.
 Contributing to SAGEmath
 Shadow puppet analogy for entanglement
 Books for contest math
 Analysing simple games
 Linear algebraic proof of the handshaking lemma
 Historical contemporaries
 Rota's twelvefold way
 Counting necklackes with unique elements
 Decomposition of projective space
 Childhood: Playing pokemon gold in japanese
 Tensor is a thing that transforms like a tensor
 Tensor Hom adjunction
 Schur's lemma
 Daughters of destiny
 Stuff I learnt in 2020
 Line bundles, a high level view as I understand them today
 Conversations with a wood carver
 Discrete Riemann Roch
 Conversation with Olaf Klinke
 Topological groups and languages
 The mnemonica stack (TODO)
 Conversation with Alok about how I read
 KMP (Knuth, Morris, Pratt) (TODO)
 Reading C declarations
 Make mnemonics
 Vandermonde and FFT
 Thoughts on blitz chess: 950 ELO
 Periodic tables and make illegal states unrepresentable
 questions on the structure of graphs
 Combinations notation in bijective combinatorics
 Arguments for little endian
 Expectiles
 Depth first search through linear algebra (TODO)
 2SAT
 Longest increasing subsequence, step by step (TODO)
 On reading how to rule (TODO)
 Strongly Connected Components via Kosaraju's algorithm
 Articulation points
 Disjoint set union
 Making GDB usable
 Bouncing light clock is an hourglass
 Euler tours
 Representation theory of the symmetric group (TODO)
 Maximum matchings in bipartite graphs
 padics, 2's complement, intuition for bit fiddling
 Diameter of a tree
 Catalan numbers as popular candidate votes (TODO)
 The chromatic polynomial (TODO)
 Structure theory of finite endofunctions
 Number of paths in a DAG
 Set partitions
 Integer partitions: Recurrence
 Stars and bars by direct bijection
 DFS and topological sorting
 Tournaments
 Matching problems (TODO)
 Four fundamental subspaces
 WHO list of essential medicines (TODO)
 why is
int i = i
allowed in C++?  Kakoune cheatsheet
 Assembly IDE
 Cohomology is like holism
 Flows (TODO)
 Amortized analysis
 Shelly Kegan: death  Suicide and rationality (TODO)
 Sam harris and jordan peterson: Vancouver 1 (TODO)
 Correctness of binary search

readlink f
to access file path  rank/select as compress/decompress
 Remembering Eulerian and Hamiltonian cycles
 Nice way to loop over an array in reverse
 Dynamic Programming: Erik Demaine's lectures
 Accuracy vs precision
 Why is the gradient covariant?
 Politicization of science
 Multi ꙮ cular O: ꙮ / Eye of cthulu
 You can't measure the one way speed of light
 Show me the hand strategy
 Words that can be distinguished from letters if we know the sign of the permutation
 Easy times don't create weak people, they just allow weak people to survive.
 Multiplicative weights algorithm (TODO)
 How to fairly compare groups
 Bijection from
(0, 1)
to [0, 1]
 Rene Girard
 Noam Chomsky on anarchism (TODO)
 Slavoj Zizek: Violence
 Poverty: Who's to blame?
 Learn Zig in Y minutes
 The algebraic structure of the 'nearest smaller number' question
 Why loss of information is terrifying: Checking that a contextfree language is regular is undecidable
 Sciences of the artificial
 Numbering nodes in a tree
 Number of vertices in a rooted tree
 Median minimizes L1 norm
 LISP quine
 A slew of order theoretic and graph theoretic results
 Thebes
 Beethoven
 Neko to follow your cursor around
 Non commuting observables: Light polarization
 Statement expressions and other GCC C extensions
 A quick look at impredicativity
 Data oriented programming in C++
 Retro glitch
 SSA as linear typed language
 Nix weirdness on small machines
 Autodiff over derivative of integrals
 Proof of projective duality
 Preventing the collapse of civilization
 Violent deaths in ancient societies (TODO)
 An elementary example of a thing that is not a vector
 Elementary probability theory (TODO)
 The handshaking lemma
 Git for pure mathematicians
 Mutorch
 Computing the smith normal form
 Laziness for C programmers
 Exact sequence of pointed sets
 What is a syzygy?
 Under the spell of Leibniz's dream
 Normal operators: Decomposition into Hermitian operators
 Readable pointers
 The grassmanian, handwavily
 Lie bracket as linearization of conjugation
 Computational Origami
 Katex in duktape
 Kebab case
 Localization: Introducing epsilons (TODO)
 NaN punning: Storing integers in doubles in JavaScript
 Offline Documentation
 Using Gurobi
 osqp: convex optimizer in 6000 LoC
 stars and bars by generating functions
 This is not a place of honor
 Topological proof of infinitude of primes
 Burnside Theorem
 The Ise Grand shrine
 Edward Kmett's list of useful math
 Cokernel is not sheafy
 Von neumann: foundations of QM
 Discrete schild's ladder
 Derivative of step is dirac delta
 Extended euclidian algorithm
 In a PID, all prime ideals are maximal, geometrically
 Prime numbers as maximal among principal ideals
 Axiom of Choice and Zorn's Lemma
 Local ring in terms of invertibility
 Nullstellensatz for schemes
 Perspectives on Yoneda
 Germs, Stalks, Sheaves of differentiable functions
 Connectedness in terms of continuity
 Intuition for limits in category theory
 Finite topologies and DFS numbering
 Categorical definition of products in painful detail
 Why is the spectrum of a ring called so?
 Ergo proxy
 Satisfied and frustrated equations
 Combinatorial intuition for Fermat's little theorem
 An incorrect derivation of special relativity in 1D
 The geometry and dynamics of magnetic monopoles
 Sanskrit and Sumerian
 Writing Cuneiform
 The code of hammurabi
 The implicit and inverse function theorem
 Whalesong hyperbolic space in detail
 Motivating Djikstra's
 Intuitions for hyperbolic space
 Product of compact spaces in compact
 Hyperbolic groups have solvable word problem
 Elementary uses of Sheaves in complex analysis
 Snake lemma
 Kernel, cokernel, image
 The commutator subgroup
 Simplicity of A5 using PSL(2, 5)
 A5 is not solvable
 Complex orthogonality in terms of projective geometry
 Arithmetic sequences, number of integers in a closed interval
 The arg function, continuity, orientation
 Odd partitions, unique partitions
 Continued fractions, mobius transformations
 Permutationsandlyndonfactorization
 Graphs are preorders
 Parallelisable version of maximum sum subarray
 Thoughts on implicit heaps
 Discriminant and Resultant
 Polynomial root finding using QR decomposition
 A hacker's guide to numerical analysis
 Mobius inversion on Incidence Algebras
 Finite differences and Umbral calculus
 Permutahedron
 Lyndon + Christoffel = Convex Hull
 Geometric proof of
e^x >= 1+x
, e^(x) >= 1x
 Ranking and Sorting
 Proof of minkowski convex body theorem
 Burrows Wheeler
 Intuitionstic logic as a Heytig algebra
 Edit distance
 Evolution of bee colonies (TODO)
 Best practices for array indexing
 Algebraic structure for vector clocks
 Networks are now faster than disks
 Einsteinde Haas effect
 Rankselect as adjunction
 Bounding chains: uniformly sample colorings
 Coupling from the past
 Word problems in Russia and America
 Encoding mathematical hieararchies
 Learning code by hearing it
 Your arm can be a spinor
 Self modifying code for function calls: Look ma, I don't need a stack!
 Adjunctions as advice
 Reversible computation as groups on programs
 Blazing fast math rendering on the web
 VC dimension
 Symplectic version of classical mechanics
 Theorems for free
 How to reason with halfopen intervals
 How does one build a fusion bomb?
 Christoffel symbols, geometrically
 A natural vector space without an explicit basis
 Cache oblivious B trees
 KrohnRhodes decomposition
 Proving block matmul using program analysis
 Why I like algebra over analysis

using
for cleaner function type typedefs  A walkway of lanterns (TODO)
 Natural transformations
 The hilarious commentary by dinosaure in OCaml git
 How to link against MLIR with CMake
 Energy as triangulaizing state space
 The cutest way to write semidirect products
 My Favourite APLisms
 Proof of chinese remainder theorem on rings
 monic and epic arrows
 The geometry of Lagrange multipliers
 Efficient tree transformations on GPUs (TODO)
 Things I wish I knew when I was learning APL
 Every ideal that is maximal wrt. being disjoint from a multiplicative subset is prime
 Getting started with APL
 SpaceChem was the best compiler I ever used
 Mnemonic for Kruskal and Prim
 Legendre transform
 Cartesian Trees
 DFS numbers as a monotone map
 Self attention? not really
 Coarse structures
 Matroids for greedy algorithms (TODO)
 Grokking Zariski
 My preferred version of quicksort
 Geometric proof of Cauchy Schwarz inequality
 Dataflow analysis using Grobner basis
 Fenwick trees and orbits
 Dirichlet inversion
 Incunabulum for the 21st century: Making the J interpreter compile in 2020
 An example of a sequence whose successive terms get closer together but isn't Cauchy (does not converge)
 Krylov subspace method
 Good reference to the Rete pattern matching algorithm
 Leapfrog Integration
 Comparison of forward and reverse mode AD
 An invitation to homology and cohomology, Part 1  Homology
 An invitation to homology and cohomology, Part 2  Cohomology
 Stuff I learnt in 2019
 A motivation for padic analysis
 Line of investigation to build physical intuition for semidirect products
 Topology is really about computation  part 2
 Topology is really about computation  part 1
 PSLQ algorithm: finding integer relations between reals
 Geometric characterization of normal subgroups
 Handy characterization of adding an element into an ideal, proof that maximal ideal is prime
 Radical ideals, nilpotents, and reduced rings
 My disenchantment with abstract interpretation
 Computing equivalent gate sets using grobner bases
 The janus programming language  Time reversible computation

A = B
 A book about proofs of combinatorial closed forms  Generating
k
bitsets of a given length n
:  Bondi kcalculus
 Topology as an object telling us what zerolocus is closed:
 Vivado toolchain craziness
 What the hell is a Grobner basis? Ideals as rewrite systems
 Lie bracket versus torsion
 Blog post: Weekend paper replication of STOKE, the stochastic superoptimizer
 Collapsing
BlockId
, Label
, Unique
:  Spatial partitioning data structures in molecular dynamics
 Vector: Arthur Whitney and text editors
 Representing CPS in LLVM using the
@coro.*
intrinsics  Bug in the LLVM code generator: Lowering of
MO_Add2
and MO_AddWordC
 Discrete random distributions with conditioning in 20 lines of haskell
 Everything you know about word2vec is wrong
 Hamiltonian monte carlo, leapfrog integrators, and sympletic geometry
 Small Haskell MCMC implementation
 The smallest implementation of reverse mode AD (autograd) ever:
 Timings of passes in GHC, and low hanging fruit in the backend:
 Varargs in GHC:
T7160.hs
 Debugging debug info in GHC
 GHC LLVM code generator: Switch to unreachable
 Concurrency in Haskell
 Handy list of differential geometry definitions
 Lazy programs have space leaks, Strict programs have time leaks
 Presburger arithmetic can represent the Collatz Conjecture
 Using compactness to argue about covers
 Japanese Financial Counting system
 Stephen wolfram's live stream

Cleave
as a word has some of the most irregular inflections  McCune's single axiom for group theory

Word2Vec
C code implements gradient descent really weirdly  Arthur Whitney: dense code
 How does one work with arrays in a linear language?
 Linear optimisation is the same as linear feasibility checking
 Quantum computation without complex numbers
 Linguistic fun fact: Comparative Illusion
 Longform posts:
 Emacs Cheat Sheet
 Coq Cheat Sheet
 Writing Cheat Sheet
 Latex Cheat Sheet
 Architecture Cheat Sheet
 Recipes Cheat Sheet
 History Cheat Sheet
 Words Cheat Sheet
 Clojure Sheat Sheet
 Big list of quotes
 Empathy
 Vim Cheat Sheet
 Big list of Chess
 Big list of shitposting
 Big list of Breakdance
 Big list of Cardistry
 Poems to memorize
 X86 Cheat Sheet
 Common Lisp Cheat Sheet
 Agda Cheat Sheet
 Don't Try
 Big list of Hacker news
 Hair in a bun with stick
 Big list of shuffle dancing
 Big list of tmux
 Favourite Demoscenes