Siddharth Bhat

• Leave me your thoughts anonymously / Email me: bollu@pixel-druid.com
• Github / Math.se / Resume / Link hoard / Sheet music
• RSS feed
• It's useful to finish things.

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