A Universe of Sorts (Siddharth Bhat)



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