Tangent space Updated 2025-07-16
TODO what's the point of it.
Bibliography:
Backstory Updated 2025-07-16
Supernatural martial arts Updated 2025-07-16
Shame that the Chinese in the lat 20th early 21st like that bullshit so much. It just weakens everything. Just imaginge those works with more realistic fighting! Would be amazing.
Lean (proof assistant) Updated 2026-01-30
Source code:
The way Lean and Coq mix programming and mathematics is a thing of great beauty. This is especially notable in lean as you start to play with with things such as:
  • partialenv lean functions, and using terminates_by to prove that certain functions terminate. Lean requires explicitly known if functions terminate or not to be able to use them in proofs.
  • noncomputable functions. Lean allows you to define mathematical functions which you can't actually execute, and it tracks that explicitly
Their 2025 current installation method is bullshit, recommends VS Code extension on Ubuntu. Lol.
From CLI:
curl https://elan.lean-lang.org/elan-init.sh -sSf | sh
source $HOME/.elan/env
Then when you run:
lean
it downloads the lean executable for you. Insane shit, could only come from a Microsoft mindset.
Coursera Updated 2025-07-16
Some courses at least allow you to see material for free, e.g.: www.coursera.org/learn/quantum-optics-single-photon/lecture/UYjLu/1-1-canonical-quantization. Lots of video focus as usual for MOOCs.
It is extremely hard to find the course materials without enrolling, even if enrolling for free! By trying to make money, they make their website shit.
The comment section does have a lot of activity: www.coursera.org/learn/statistical-mechanics/discussions/weeks/2! Nice. And works like a proper issue tracker. But it is also very hidden.
EdX Updated 2025-07-16
As of 2022:
  • can't see course material before start date. Once archived, you can see it but requires login...
  • on free mode, limited course access
Fuck that.
Also, they have an ICP.
November 2023 course search:

There are unlisted articles, also show them or only show them.