A Universe of Sorts (Siddharth Bhat)



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