A Universe of Sorts

Siddharth Bhat




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