A Universe of Sorts (Siddharth Bhat)



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