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