A Universe of Sorts (Siddharth Bhat)



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