A Universe of Sorts

Siddharth Bhat




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