A Universe of Sorts

Siddharth Bhat

  1. Stuff I learnt in 2022
  2. You don't know jack about data races
  3. Training a custom model for Lean4
  4. Stratified synthetsis
  5. Libtpu
  6. Mutual recursion elaboration in Lean
  7. Subject reduction in Lean
  8. Big list of GNU Binutils
  9. Automatically building a JIT compiler
  10. Model theory
  11. Mathematical logic: real closed fields
  12. Sturm's theorem
  13. CMake configure_file
  14. List symbols in a file
  15. Axiom K versus UIP
  16. Linear vs uniqueness types
  17. Better shell history with atuin
  18. Better git diff with delta
  19. Any model of lean must have all inductives
  20. Index over the past, fiber over the future
  21. Kripke style logical relations (TODO)
  22. Impredicativity
  23. Type formers need not be injective
  24. There cannot be a type of size the universe:
  25. The dependently typed expression problem
  26. Rotation distance as a metric on binary trees
  27. Motivation for modal logic
  28. Scones
  29. Presheaf models of type theory
  30. Weighted limits via collages
  31. Disjoint Coproduct
  32. Universal coproduct / stable under pullback
  33. Leibniz Equality in Lean4
  34. Strong normalization of STLC
  35. Subobject classifiers of NFinSetN \to FinSet, or precosheaf of FinSetFinSet
  36. Dimensions versus units
  37. HoTTesT: Identity types
  38. Philosophy of History
  39. Left and right adjoints to inverse image [TODO ]
  40. Paredit via adjoints
  41. Less than versus Less than or equals over Z
  42. Allegories and Categories
  43. Partial function as span
  44. Post's Problem [WIP ]
  45. Turing degree
  46. Ultraproducts in Logic [WIP ]
  47. Pivot tables are indexed categories [WIP ]
  48. Kleene Tree [WIP ]
  49. Compactness theorem as compactness of stone spaces [WIP ]
  50. Setting up windows box on google cloud
  51. Proof that there is a TM whose halting is independent of ZFC
  52. Contradiction from non-positive occurence
  53. The constructible universe L
  54. Scrivano for note taking
  55. Godel completeness theorem
  56. Uniform proofs, focused proofs, polarization, logic programming
  57. Why cut elimination?
  58. Forcing to add a function
  59. Diaconescu's theorem
  60. Forcing machinery
  61. Partial Evaluation, Chapter 3
  62. Partial Evaluation, Chapter 1
  63. Diagonal lemma for monotone functions
  64. Cantor Schroder Bernstein via fixpoint
  65. Maximal Ideals of Boolean Algebras are Truth Values
  66. Crash course on DCPO: formalizing lambda calculus
  67. Resolution algorithm for propositional logic
  68. Completeness for first order logic
  69. Compactness theorem of first order logic
  70. WIP: Tarski's undefinability theorem
  71. WIP: Conservative extension to type theory
  72. First order logic: Semantics
  73. full abstraction in semantics (TODO)
  74. You could have invented Sequents
  75. Fibrational category theory, sec 1.1, sec 1.2
  76. Simple Type Theory via Fibrations
  77. Realisability models
  78. Naming left closed, right open with start/stop
  79. Nested vs mutual inductive types:
  80. MiniSketch [TODO ]
  81. Finger trees data structure [TODO ]
  82. HAMT data structure [TODO ]
  83. Embedding HOL in Lean
  84. Module system for separate compilation
  85. Second order arithmetic
  86. Lean4 Dev Meeting
  87. Categorical model of dependent types
  88. How should relative changes be measured
  89. Logic of bunched implications
  90. Coends
  91. Natural Transformations as ends
  92. Ends and diagonals
  93. Parabolic dynamics and renormalization
  94. Quantifiers as adjoints
  95. TLDP pages for bash conditionals
  96. Remainder, Modulo
  97. Parameters cannot be changed anywhere , not just in return location
  98. LCNF
  99. Predicative v/s Impredicative: On Universes in Type Theory
  100. Testing infra in Lean4
  101. Autocompletion in Lean4
  102. Inductive types
  103. Parameter verus Index
  104. HNF versus WHNF
  105. Different types of arguments in Lean4:
  106. Big list of lean tactics
  107. Hyperdoctrine
  108. Fungrim
  109. Category where coproducts of computable things is not computable
  110. Homotopy continuation
  111. Relationship between linearity and contradiction
  112. Monads from Riehl
  113. Combinatorial Cauchy Schwarz
  114. Bezout's theorem
  115. Example for invariant theory
  116. Counterexample to fundamental theorem of calculus?
  117. Why a sentinel of -1 is sensible
  118. Data structure to maintain mex
  119. Scatted algebraic number theory ideas: Ramification
  120. Coreflection
  121. Better man Pages via info
  122. The Zen of juggling three balls
  123. Example of lattice that is not distributive
  124. Patat
  125. Common Lisp LOOP Macro
  126. Mitchell-Bénabou language
  127. Hyperdoctrine
  128. Why is product in Rel not cartesian product?
  129. simp in Lean4
  130. Big list of Lean4 TODOS
  131. unsafePerformIO in Lean4:
  132. Big List of Lean4 FAQ
  133. Sheaves in geometry and logic 1.2: Pullbacks
  134. Sheaves in geometry and logic 1.3: Characteristic functions of subobjects
  135. Common Lisp Debugging: Clouseau
  136. Drawabox: Lines
  137. Common Lisp Beauty: paths
  138. Logical Predicates (OPLSS '12)
  139. Logical Relations (Sterling)
  140. Pointless topology: Frames
  141. Introduction to substructural logics: Ch1
  142. Integrating against ultrafilers
  143. wegli: Neat tool for semantically grepping C++
  144. Mostowski Collapse
  145. Spaces that have same homotopy groups but not the same homotopy type
  146. Fundamental group functor does not preserve epis
  147. Epi in topological spaces
  148. Permutation models
  149. Almost universal class
  150. Godel operations
  151. Orthogonal Factorization Systems
  152. Orthogonal morphisms
  153. Locally Presentable Category
  154. Remez Algorithm
  155. Permission bits reference
  156. Papers on Computational Group Theory
  157. Kan Extensions: Key idea
  158. Interleaved dataflow analysis and rewriting
  159. Central variable as focal
  160. Wilson's theorem
  161. General enough special cases
  162. XOR and AND relationship
  163. Geometry of complex integrals
  164. Green's functions
  165. CP trick: writing exact counting as counting less than
  166. CP trick: Heavy Light Decomposition euler tour tree
  167. Counting with repetitions via pure binomial coefficients
  168. Fundamental theorem of homological algebra [TODO ]
  169. Projective modules in terms of universal property
  170. How ideals recover factorization [TODO ]
  171. Centroid of a tree
  172. Path query to subtree query
  173. Pavel: bridges, articulation points for UNDIRECTED graphs
  174. Segtree: range update, point query [TODO ]
  175. Monadic functor
  176. Injective module
  177. Proof that Spec(R)Spec(R) is a sheaf [TODO ]
  178. Projections onto convex sets
  179. LM algorithm for nonlinear least squares
  180. Backward dataflow and continuations
  181. Coordinate compression with set and vector
  182. Hilbert polynomial and dimension
  183. Cost of looping over all multiples of ii for ii in 11 to NN
  184. Stuff I learnt in 2021
  185. Cayley hamilton for 2x2 matrices in sage via AG
  186. LispWorks config
  187. Birkhoff Von Neumann theorem
  188. Latin Square
  189. Assignment Problem
  190. Interpolating homotopies
  191. Example where MIP shows extra power over IP
  192. Lazy reversible computation?
  193. Theorem coverage as an analogue to code coverage
  194. Lazy GPU programming
  195. Projections onto convex sets [TODO ]
  196. BGFS algorithm for unconstrained nonlinear optimization [TODO ]
  197. LM algorithm for nonlinear least squares [TODO ]
  198. Backward dataflow and continuations
  199. The tyranny of structurelessness
  200. Simple Sabotage Field Manual
  201. Counting permutations with #MAXSAT
  202. Coloring cat output with supercat
  203. Reader monoid needs a hopf algebra?! [TODO ]
  204. Monads mnemonic
  205. Card stacking
  206. Representation theory for particle physics [TODO ]
  207. SSH into google cloud
  208. Comma & Semicolon in index notation
  209. Spin groups
  210. How to write in biblical style?
  211. Undefined behaviour is like compactification [TODO ]
  212. God of areppo
  213. Classification of lie algebras, dynkin diagrams
  214. Weird free group construction from adjoint functor theorem
  215. bashupload
  216. When are the catalan numbers odd
  217. Discrete probability [TODO ]
  218. Geodesic equation, Extrinsic
  219. Connections, take 2
  220. Dropping into tty on manjaro/GRUB
  221. Why the zero set of a continuous function must be a closed set
  222. Derivatives in diffgeo
  223. Building stuff with Docker
  224. Lie derivative versus covariant derivative
  225. The Tor functor
  226. Sum of quadratic errors
  227. Hip-Hop and Shakespeare
  228. Write thin to write well
  229. Hidden symmetries of alg varieties
  230. fd for find
  231. Thu Morse sequence for sharing
  232. Elementary and power sum symmetric polynomials
  233. Projective spaces and grassmanians in AG
  234. Mnemonic for why eta is unit:
  235. Fundamental theorem of galois theory
  236. Counter-intuitive linearity of expectation [TODO ]
  237. Metis
  238. Tooling for performance benchmarking
  239. Normal field extensions
  240. Eisenstein Theorem for checking irreducibility
  241. Gauss Lemma for polynomials
  242. How GHC does typeclass resolution
  243. Defining continuity covariantly
  244. Why commutator is important for QM
  245. Deriving pratt parsing by analyzing recursive descent [TODO ]
  246. Level set of a continuous function must be closed
  247. HPNDUF - Hard problems need design up front!
  248. Separable Extension is contained in Galois extension
  249. Primitive element theorem
  250. Separable extension via embeddings into alg. closure
  251. Separable extensions via derivation
  252. Irreducible polynomial over a field divides any polynomial with common root
  253. Galois extension
  254. Separability of field extension as diagonalizability
  255. Motivation for the compact-open topology
  256. Example of covariance zero, and yet "correlated"
  257. Hypothesis Testing
  258. Dumb mnemonic for remembering adjunction turnstile
  259. Delta debugging
  260. Tidy Data
  261. Normal subgroups through the lens of actions
  262. Writing rebuttals, Tobias style
  263. LCS DP: The speedup is from filtration
  264. Poisson distribution
  265. F1 or Fun : The field with one element
  266. McKay's proof of Cauchy's theorem for groups [TODO ]
  267. Odds versus probability [TODO ]
  268. ncdu for disk space measurement
  269. nmon versus htop
  270. Schrier sims --- why purify generators times coset
  271. Vyn's feeling about symmetry
  272. Convergence in distribution is very weak
  273. Class equation, P-group structure
  274. Sylow Theorem 1
  275. Fuzzing book
  276. Filtered Colimits [TODO ]
  277. Fisher Yates
  278. Bucchberger algorithm
  279. GAP permutation syntax
  280. Why division algorithm with multiple variables go bad
  281. Integral elements of a ring form a ring [TODO ]
  282. "Cheap" proof of euler characteristic
  283. Siefert Algorithm [TODO ]
  284. Cap product [TODO ]
  285. Cup product [TODO ]
  286. Colimits examples with small diagram categories
  287. Limits examples with small diagram categories
  288. Classification of compact 2-manifolds [TODO ]
  289. Gauss, normals, fundamental forms [TODO ]
  290. Second fundamental form
  291. Shape operator [TODO ]
  292. Theorem Egregium / Gauss's theorem (Integrating curvature in 2D) [TODO ]
  293. Integrating Curvature in 1D [TODO ]
  294. Fundamental theorem of symmetric polynomials
  295. DP over submasks
  296. Dual of Planar Euler graph is bipartite
  297. Yoneda preserves limits
  298. Separable Polynomials and extensions
  299. Limits of a functor category are computed pointwise.
  300. a + b = (a or b) + (a and b)
  301. Intuition for why choosing closed-closed intervals of [1..n] is (n+1)C2(n+1)C2
  302. Thoughtful discussion on the limits of safe spaces
  303. Semidirect product: Panning and Zooming
  304. Longest Convex Subsequence DP
  305. Representation theory of SU(2)SU(2) [TODO ]
  306. Why quaternions work better
  307. DFA to CFG via colimits?
  308. Why pointless topology is powerful
  309. Denotational semantics in a few sentences
  310. Monge Matrix
  311. Fixpoint as decorator
  312. Combinatorial generation algorithms
  313. Perform DP on measures, not indexes.
  314. Alternative version of Myhill-Nerode
  315. Polya Enumeration
  316. Weighted Burnside Lemma
  317. Cycle index polynomial
  318. Mnemonics For Symmetric Polynomials
  319. Uses of minimal string rotation
  320. Suffix Automata
  321. Simpson's Paradox
  322. Myhill Nerode Theorem
  323. Linearity of expectation for sampling
  324. Dedekind MacNiellie
  325. Good and bad combinatorics: intro to counting
  326. Expected number of turns to generate all numbers 1..N (TODO)
  327. Diameter in single DFS (TODO)
  328. Min cost flow (TODO)
  329. Clojure: minimal makefile for REPL driven dev with Neovim
  330. Delimited continuations
  331. Never forget monic again
  332. Weird canonical example of monic and epic: left/right shift
  333. Playing guitar: being okay with incorrect chords
  334. Sparse table
  335. Duval's algorithm
  336. Amortized complexity from the verifier perspective
  337. Relationship betwee permutations and runs
  338. Brouwer's fixed point theorem
  339. XOR on binary trie
  340. Inconvergent: beautiful generative art
  341. Prefix/Border function
  342. Shortest walk versus shortest path
  343. Minimal tech stack
  344. FFT
  345. codeforces rating of some GMs
  346. Continuum TTRPG
  347. Words to know in target language
  348. DP on subarrays
  349. Vis editor cheat sheet
  350. Mean, Median and Jensen's
  351. The similarity between labellings and representations
  352. L1 norm is greater than or equal to L2 norm
  353. Z algorithm
  354. For a given recurrence, what base cases do I need to implement?
  355. Number of distinct numbers in a partition
  356. Splitting f(x)=yf(x) = y into indicators
  357. Why searching for divisors upto sqrt(n) works
  358. Heuristics for the prime number theorem
  359. Sum of absolute differences of an array
  360. GCD is at most difference of numbers
  361. implementing GCD and LCM
  362. Centroid of a tree
  363. Center of a tree
  364. Image unshredding as hamiltonian path
  365. Distance between lines in nD
  366. lower_bound binary search with closed intervals
  367. Sliding window implementation style
  368. Kawaii implementation of x = min(x, y)
  369. CSES: Counting Towers
  370. Smallest positive natural which can't be represented as sum of any subset of a set of naturals
  371. Example of RVs that are pairwise but not 3-way independent.
  372. Notes on Liam O Connor's thesis: Cogent
  373. C++ lower_bound, upper_bound API
  374. Books that impart mental models
  375. Subarrays ~= prefixes
  376. Operations with modular fractions
  377. Modular inverse calculation
  378. The number of pairs (a,b) such that ab≤x is O(xlogx)
  379. DP as path independence
  380. Binary search to find rightmost index which does not possess some property
  381. Correctness of lower_bound search with half-open intervals
  382. Greedy Coin change: proof by probing
  383. Clean way to write burnside lemma
  384. The groupoid interpretation of type theory
  385. Mnemonics for free = left adjoint
  386. Where to scratch a cat
  387. Mnemonic for Specht module actions
  388. Quotes from 'Braiding Sweetgrass'
  389. Transfinite recursion: Proof
  390. Transfinite induction: Proof
  391. Thoughts on playing Em-Bm
  392. An explanation for why permutations and linear orders are not naturally isomorphic
  393. We can't define choice for finite sets in Haskell!
  394. Geomean is scale independent
  395. Thoughts on playing Em Bm.
  396. Induction on natural numbers cannot be derived from other axioms
  397. Ordinals and cardinals
  398. Musing about Specht modules
  399. Every continuous function on [a,b][a, b] attains a maximum
  400. Invisible cities
  401. Associativity of addition in cubicaltt
  402. Etymology of fiber bundle FEBF \rightarrow E \rightarrow B
  403. Galois correspondence, functorially
  404. CubicalTT: sharpening thinking about indexed functions
  405. Functors to motivate adjuntions
  406. Madoka Magica: plot thoughts
  407. Chain rule functorially
  408. Lagrange multipliers by algebra
  409. Specht module construction
  410. Even and odd functions through representation theory
  411. Greg egan: Orthogonal
  412. Simplicial approximation: maps can be approximated by simplicial maps (TODO)
  413. Excision (TODO)
  414. Marshall: Andrej (TODO)
  415. Limit is right adjoint to diagonal
  416. Working out why right adjoints preserve limits.
  417. Limit/Colimit/Cone/Cocone: the arrows are consistent!
  418. Representable Functors
  419. Why terminal object is a limit
  420. Excluded middle is not false in intuitionistic logic
  421. Yoneda Lemma and embedding
  422. GHCID
  423. Character theory
  424. Cofibration
  425. Emily Riehl Contrability as uniqueness
  426. Cofactor as derivative of determinant
  427. Homology, the big picture
  428. Normaliztion by evaluation (TODO)
  429. Legal Systems very different from ours
  430. Lefschetz fixed point theorem (TODO)
  431. Shrinking wedge of circles / Hawaiian earring (TODO)
  432. Simplicial approxmation of maps (TODO)
  433. Lebesgue number lemma (TODO)
  434. Lean internals Cheat Sheet
  435. MicroUI
  436. Proof of tree having (V-1) edges
  437. Creating PDFs to read code
  438. Bias and gain
  439. Barycentric subdivision: edge length decreases
  440. Homotopic maps produce same singular homology: Intuition
  441. Singular homology: induced homomorphism
  442. Demoscene tools
  443. Binaural Beat
  444. Low pass filter by delaying
  445. Octaves are double frequency apart (TODO)
  446. Bias and gain
  447. Show, don't tell
  448. Try and think of natural transformations as intertwinings
  449. Subobject classifier measures how much we need to pay to access fact
  450. Spectral norm of Hermitian matrix equals largest eigenvalue (TODO)
  451. Penrose cohomology [TODO ]
  452. Bicycle wheel proof of Gauss Bonnet (TODO)
  453. What is Levi Cevita trying to describe (TODO)
  454. Torsion as giving monodromy of path lifts (TODO)
  455. Cartan's spiral staircase (TODO)
  456. Weingarten map
  457. When maps cannot be lifted to the universal cover
  458. Nets from Munkres (TODO)
  459. Limit point compactness from Munkres
  460. Proof of Heine Borel from Munkres (compact iff closed, bounded)
  461. Alexandrov topology
  462. Zeroth singular homology group: Intuition
  463. Examples of fiber products / pullbacks
  464. Covariant derivative
  465. Clackety sounds: bucklespring
  466. Submersions and immersions
  467. Ehrsmann connection
  468. Quotes from the culture
  469. Lie bracket commutator as infinitesimal conjugation
  470. Thoughts on proof of fundamental group of unit circle
  471. Pasting lemma
  472. Tensoring with base ring has no effect
  473. Seeing the semidirect product of the dihedral group.
  474. Animating rotations with quaternion curves
  475. Mnemonic for hom-tensor and left-right adjoints
  476. Construction of tensor product: Atiyah macdonald
  477. Recovering topology from sheaf of functions: Proof from Atiyah Macdonald
  478. Urhyson's lemma
  479. Compact Hausdorff spaces are normal
  480. Stone representation theorem: Proof from Atiyah Macdonald
  481. Covariant Hom is left exact
  482. Internal versus External semidirect products
  483. Splitting of semidirect products in terms of projections
  484. Tensor is right exact
  485. Semidirect product as commuting conditions
  486. Exact sequences for semidirect products; fiber bundles
  487. Semidirect product is equivalent to splitting of exact sequence
  488. Intro to topological quantum field theory
  489. Non examples of algebraic varieties
  490. Nilradical is intersection of all prime ideals
  491. Exactness of modules is local
  492. Quotient by maximal ideal gives a field
  493. Ring of power series with infinite positive and negative terms
  494. Mean value theorem and Taylor's theorem. (TODO)
  495. Cayley Hamilton
  496. Nakayama's lemma
  497. Vector fields over the 2 sphere
  498. Learning to talk with your hands
  499. Lovecraftisms
  500. Hairy ball theorem from Sperner's Lemma (TODO)
  501. CS and type theory: Talks by vovodesky
  502. Hilbert basis theorem for polynomial rings over fields (TODO)
  503. Covering spaces
  504. Wedge Sum and Smash Product
  505. Quotient topology
  506. CW Complexes and HEP
  507. Stable homotopy theory
  508. Simply connected spaces
  509. Finitely generated as vector space v/s algebra:
  510. Weak and Strong Nullstllensatz
  511. Screen recording for kakoune pull request
  512. Intuition for why finitely presented abelian groups are isomorphic to product of cyclics
  513. Euler characteristic of sphere
  514. John Conway: The symmetries of things
  515. Semidirect product mnemonic
  516. Non orthogonal projections
  517. Why did maxwell choose his EM wave to be light?
  518. Fast string concatenation in python3
  519. Split infinitive
  520. Yoneda from string concatenation
  521. Right Kan extensions as extending the domain of a functor
  522. Non standard inner products and unitarity of representations
  523. take at most 4 letters from 15 letters.
  524. Flat functions
  525. Hopf Algebras and combinatorics
  526. Butcher group
  527. Neovim frontends
  528. A semidirect product worked on in great detail
  529. Direct and Inverse limits
  530. LEAN 4 overfrom from LEAN together 2021
  531. BLM master thesis
  532. Hololive subculture
  533. RSK correspondence for permutations
  534. Djikstra's using a segtree
  535. Markov and chebyshev from a measure theoretic lens
  536. Among any 51 integers, that are 2 with squares having equal value modulo 100
  537. 1n+2n++(n1)n1^n + 2^n + \dots + (n-1)^n is divisible by nn for odd nn
  538. 103n+110^{3n+1} cannot be written as sum of two cubes
  539. Coq-club: the meaning of a specification
  540. SQLite opening
  541. Old school fonts
  542. Stalking syzigies on hackernews
  543. Conditional probability is neither causal nor temporal
  544. Hook length formula
  545. The tyranny of light
  546. Muirhead's inequality
  547. Rearrangement inequality
  548. Triangle inequality
  549. The Heather subculture
  550. Frobenius Kernel
  551. Galois theory by "Abel's theorem in problems and solutions"
  552. Galois theory perspective of the quadratic equation
  553. Burnside lemma by representation theory.
  554. Contributing to SAGEmath
  555. Shadow puppet analogy for entanglement
  556. Books for contest math
  557. Analysing simple games
  558. Linear algebraic proof of the handshaking lemma
  559. Historical contemporaries
  560. Rota's twelvefold way
  561. Counting necklackes with unique elements
  562. Decomposition of projective space
  563. Childhood: Playing pokemon gold in japanese
  564. Tensor is a thing that transforms like a tensor
  565. Tensor Hom adjunction
  566. Schur's lemma
  567. Daughters of destiny
  568. Stuff I learnt in 2020
  569. Line bundles, a high level view as I understand them today
  570. Conversations with a wood carver
  571. Discrete Riemann Roch
  572. Conversation with Olaf Klinke
  573. Topological groups and languages
  574. The mnemonica stack (TODO)
  575. Conversation with Alok about how I read
  576. KMP (Knuth, Morris, Pratt) (TODO)
  577. Reading C declarations
  578. Make mnemonics
  579. Vandermonde and FFT
  580. Thoughts on blitz chess: 950 ELO
  581. Periodic tables and make illegal states unrepresentable
  582. questions on the structure of graphs
  583. Combinations notation in bijective combinatorics
  584. Arguments for little endian
  585. Expectiles
  586. Depth first search through linear algebra (TODO)
  587. 2-SAT
  588. Longest increasing subsequence, step by step (TODO)
  589. On reading how to rule (TODO)
  590. Strongly Connected Components via Kosaraju's algorithm
  591. Articulation points
  592. Disjoint set union
  593. Making GDB usable
  594. Bouncing light clock is an hourglass
  595. Euler tours
  596. Representation theory of the symmetric group (TODO)
  597. Maximum matchings in bipartite graphs
  598. p-adics, 2's complement, intuition for bit fiddling
  599. Diameter of a tree
  600. Catalan numbers as popular candidate votes (TODO)
  601. The chromatic polynomial (TODO)
  602. Structure theory of finite endo-functions
  603. Number of paths in a DAG
  604. Set partitions
  605. Integer partitions: Recurrence
  606. Stars and bars by direct bijection
  607. DFS and topological sorting
  608. Tournaments
  609. Matching problems (TODO)
  610. Four fundamental subspaces
  611. WHO list of essential medicines (TODO)
  612. why is int i = i allowed in C++?
  613. Kakoune cheatsheet
  614. Assembly IDE
  615. Cohomology is like holism
  616. Flows (TODO)
  617. Amortized analysis
  618. Shelly Kegan: death --- Suicide and rationality (TODO)
  619. Sam harris and jordan peterson: Vancouver 1 (TODO)
  620. Correctness of binary search
  621. readlink -f to access file path
  622. rank/select as compress/decompress
  623. Remembering Eulerian and Hamiltonian cycles
  624. Nice way to loop over an array in reverse
  625. Dynamic Programming: Erik Demaine's lectures
  626. Accuracy vs precision
  627. Why is the gradient covariant?
  628. Politicization of science
  629. Multi ꙮ cular O: ꙮ / Eye of cthulu
  630. You can't measure the one way speed of light
  631. Show me the hand strategy
  632. Words that can be distinguished from letters if we know the sign of the permutation
  633. Easy times don't create weak people, they just allow weak people to survive.
  634. Multiplicative weights algorithm (TODO)
  635. How to fairly compare groups
  636. Bijection from (0, 1) to [0, 1]
  637. Rene Girard
  638. Noam Chomsky on anarchism (TODO)
  639. Slavoj Zizek: Violence
  640. Poverty: Who's to blame?
  641. Learn Zig in Y minutes
  642. The algebraic structure of the 'nearest smaller number' question
  643. Why loss of information is terrifying: Checking that a context-free language is regular is undecidable
  644. Sciences of the artificial
  645. Numbering nodes in a tree
  646. Number of vertices in a rooted tree
  647. Median minimizes L1 norm
  648. LISP quine
  649. A slew of order theoretic and graph theoretic results
  650. Thebes
  651. Beethoven
  652. Neko to follow your cursor around
  653. Non commuting observables: Light polarization
  654. Statement expressions and other GCC C extensions
  655. A quick look at impredicativity
  656. Data oriented programming in C++
  657. Retro glitch
  658. SSA as linear typed language
  659. Nix weirdness on small machines
  660. Autodiff over derivative of integrals
  661. Proof of projective duality
  662. Preventing the collapse of civilization
  663. Violent deaths in ancient societies (TODO)
  664. An elementary example of a thing that is not a vector
  665. Elementary probability theory (TODO)
  666. The handshaking lemma
  667. Git for pure mathematicians
  668. Mutorch
  669. Computing the smith normal form
  670. Laziness for C programmers
  671. Exact sequence of pointed sets
  672. What is a syzygy?
  673. Under the spell of Leibniz's dream
  674. Normal operators: Decomposition into Hermitian operators
  675. Readable pointers
  676. The grassmanian, handwavily
  677. Lie bracket as linearization of conjugation
  678. Computational Origami
  679. Katex in duktape
  680. Kebab case
  681. Localization: Introducing epsilons (TODO)
  682. NaN punning: Storing integers in doubles in JavaScript
  683. Offline Documentation
  684. Using Gurobi
  685. osqp: convex optimizer in 6000 LoC
  686. stars and bars by generating functions
  687. This is not a place of honor
  688. Topological proof of infinitude of primes
  689. Burnside Theorem
  690. The Ise Grand shrine
  691. Edward Kmett's list of useful math
  692. Cokernel is not sheafy
  693. Von neumann: foundations of QM
  694. Discrete schild's ladder
  695. Derivative of step is dirac delta
  696. Extended euclidian algorithm
  697. In a PID, all prime ideals are maximal, geometrically
  698. Prime numbers as maximal among principal ideals
  699. Axiom of Choice and Zorn's Lemma
  700. Local ring in terms of invertibility
  701. Nullstellensatz for schemes
  702. Perspectives on Yoneda
  703. Germs, Stalks, Sheaves of differentiable functions
  704. Connectedness in terms of continuity
  705. Intuition for limits in category theory
  706. Finite topologies and DFS numbering
  707. Categorical definition of products in painful detail
  708. Why is the spectrum of a ring called so?
  709. Ergo proxy
  710. Satisfied and frustrated equations
  711. Combinatorial intuition for Fermat's little theorem
  712. An incorrect derivation of special relativity in 1D
  713. The geometry and dynamics of magnetic monopoles
  714. Sanskrit and Sumerian
  715. Writing Cuneiform
  716. The code of hammurabi
  717. The implicit and inverse function theorem
  718. Whalesong hyperbolic space in detail
  719. Motivating Djikstra's
  720. Intuitions for hyperbolic space
  721. Product of compact spaces in compact
  722. Hyperbolic groups have solvable word problem
  723. Elementary uses of Sheaves in complex analysis
  724. Snake lemma
  725. Kernel, cokernel, image
  726. The commutator subgroup
  727. Simplicity of A5 using PSL(2, 5)
  728. A5 is not solvable
  729. Complex orthogonality in terms of projective geometry
  730. Arithmetic sequences, number of integers in a closed interval
  731. The arg function, continuity, orientation
  732. Odd partitions, unique partitions
  733. Continued fractions, mobius transformations
  734. Permutations-and-lyndon-factorization
  735. Graphs are preorders
  736. Parallelisable version of maximum sum subarray
  737. Thoughts on implicit heaps
  738. Discriminant and Resultant
  739. Polynomial root finding using QR decomposition
  740. A hacker's guide to numerical analysis
  741. Mobius inversion on Incidence Algebras
  742. Finite differences and Umbral calculus
  743. Permutahedron
  744. Lyndon + Christoffel = Convex Hull
  745. Geometric proof of e^x >= 1+x, e^(-x) >= 1-x
  746. Ranking and Sorting
  747. Proof of minkowski convex body theorem
  748. Burrows Wheeler
  749. Intuitionstic logic as a Heytig algebra
  750. Edit distance
  751. Evolution of bee colonies (TODO)
  752. Best practices for array indexing
  753. Algebraic structure for vector clocks
  754. Networks are now faster than disks
  755. Einstein-de Haas effect
  756. Rank-select as adjunction
  757. Bounding chains: uniformly sample colorings
  758. Coupling from the past
  759. Word problems in Russia and America
  760. Encoding mathematical hieararchies
  761. Learning code by hearing it
  762. Your arm can be a spinor
  763. Self modifying code for function calls: Look ma, I don't need a stack!
  764. Adjunctions as advice
  765. Reversible computation as groups on programs
  766. Blazing fast math rendering on the web
  767. VC dimension
  768. Symplectic version of classical mechanics
  769. Theorems for free
  770. How to reason with half-open intervals
  771. How does one build a fusion bomb?
  772. Christoffel symbols, geometrically
  773. A natural vector space without an explicit basis
  774. Cache oblivious B trees
  775. Krohn-Rhodes decomposition
  776. Proving block matmul using program analysis
  777. Why I like algebra over analysis
  778. using for cleaner function type typedefs
  779. A walkway of lanterns (TODO)
  780. Natural transformations
  781. The hilarious commentary by dinosaure in OCaml git
  782. How to link against MLIR with CMake
  783. Energy as triangulaizing state space
  784. The cutest way to write semidirect products
  785. My Favourite APLisms
  786. Proof of chinese remainder theorem on rings
  787. monic and epic arrows
  788. The geometry of Lagrange multipliers
  789. Efficient tree transformations on GPUs (TODO)
  790. Things I wish I knew when I was learning APL
  791. Every ideal that is maximal wrt. being disjoint from a multiplicative subset is prime
  792. Getting started with APL
  793. SpaceChem was the best compiler I ever used
  794. Mnemonic for Kruskal and Prim
  795. Legendre transform
  796. Cartesian Trees
  797. DFS numbers as a monotone map
  798. Self attention? not really
  799. Coarse structures
  800. Matroids for greedy algorithms (TODO)
  801. Grokking Zariski
  802. My preferred version of quicksort
  803. Geometric proof of Cauchy Schwarz inequality
  804. Dataflow analysis using Grobner basis
  805. Fenwick trees and orbits
  806. Dirichlet inversion
  807. Incunabulum for the 21st century: Making the J interpreter compile in 2020
  808. An example of a sequence whose successive terms get closer together but isn't Cauchy (does not converge)
  809. Krylov subspace method
  810. Good reference to the Rete pattern matching algorithm
  811. Leapfrog Integration
  812. Comparison of forward and reverse mode AD
  813. An invitation to homology and cohomology, Part 1 --- Homology
  814. An invitation to homology and cohomology, Part 2 --- Cohomology
  815. Stuff I learnt in 2019
  816. A motivation for p-adic analysis
  817. Line of investigation to build physical intuition for semidirect products
  818. Topology is really about computation --- part 2
  819. Topology is really about computation --- part 1
  820. PSLQ algorithm: finding integer relations between reals
  821. Geometric characterization of normal subgroups
  822. Handy characterization of adding an element into an ideal, proof that maximal ideal is prime
  823. Radical ideals, nilpotents, and reduced rings
  824. My disenchantment with abstract interpretation
  825. Computing equivalent gate sets using grobner bases
  826. The janus programming language --- Time reversible computation
  827. A = B --- A book about proofs of combinatorial closed forms
  828. Generating k bitsets of a given length n:
  829. Bondi k-calculus
  830. Topology as an object telling us what zero-locus is closed:
  831. Vivado toolchain craziness
  832. What the hell is a Grobner basis? Ideals as rewrite systems
  833. Lie bracket versus torsion
  834. Blog post: Weekend paper replication of STOKE, the stochastic superoptimizer
  835. Collapsing BlockId, Label, Unique:
  836. Spatial partitioning data structures in molecular dynamics
  837. Vector: Arthur Whitney and text editors
  838. Representing CPS in LLVM using the @coro.* intrinsics
  839. Bug in the LLVM code generator: Lowering of MO_Add2 and MO_AddWordC
  840. Discrete random distributions with conditioning in 20 lines of haskell
  841. Everything you know about word2vec is wrong
  842. Hamiltonian monte carlo, leapfrog integrators, and sympletic geometry
  843. Small Haskell MCMC implementation
  844. The smallest implementation of reverse mode AD (autograd) ever:
  845. Timings of passes in GHC, and low hanging fruit in the backend:
  846. Varargs in GHC: T7160.hs
  847. Debugging debug info in GHC
  848. GHC LLVM code generator: Switch to unreachable
  849. Concurrency in Haskell
  850. Handy list of differential geometry definitions
  851. Lazy programs have space leaks, Strict programs have time leaks
  852. Presburger arithmetic can represent the Collatz Conjecture
  853. Using compactness to argue about covers
  854. Japanese Financial Counting system
  855. Stephen wolfram's live stream
  856. Cleave as a word has some of the most irregular inflections
  857. McCune's single axiom for group theory
  858. Word2Vec C code implements gradient descent really weirdly
  859. Arthur Whitney: dense code
  860. How does one work with arrays in a linear language?
  861. Linear optimisation is the same as linear feasibility checking
  862. Quantum computation without complex numbers
  863. Linguistic fun fact: Comparative Illusion
  864. Long-form posts:
  865. Emacs Cheat Sheet
  866. Coq Cheat Sheet
  867. Writing Cheat Sheet
  868. Latex Cheat Sheet
  869. Architecture Cheat Sheet
  870. Recipes Cheat Sheet
  871. History Cheat Sheet
  872. Words Cheat Sheet
  873. Clojure Sheat Sheet
  874. Big list of quotes
  875. Empathy
  876. Vim Cheat Sheet
  877. Big list of Chess
  878. Big list of shitposting
  879. Big list of Breakdance
  880. Big list of Cardistry
  881. Poems to memorize
  882. X86 Cheat Sheet
  883. Common Lisp Cheat Sheet
  884. Agda Cheat Sheet
  885. Don't Try
  886. Big list of Hacker news
  887. Hair in a bun with stick
  888. Big list of shuffle dancing
  889. Big list of tmux
  890. Favourite Demoscenes