A Universe of Sorts

Siddharth Bhat

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