A Universe of Sorts

Siddharth Bhat




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