A Universe of Sorts

Siddharth Bhat

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