A Universe of Sorts

Siddharth Bhat




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