Siddharth Bhat

• Leave me your thoughts / Chat with me / Email me: siddu.druid@gmail.com
• Github / Math.se / Resume / Link hoard
• RSS feed

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