A Universe of Sorts

Siddharth Bhat

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