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