Siddharth Bhat

• Leave me your thoughts / Chat with me / Email me: siddu.druid@gmail.com
• Github / Math.se / Resume / Link hoard
• RSS feed
• It's useful to finish things.

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