A Universe of Sorts (Siddharth Bhat)



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