A Universe of Sorts (Siddharth Bhat)



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