asdftemp
Joined 12 years ago
Joined 12 years ago
typing this up, I realize I'm not totally sure to what extent this is something that was happening before the practice vs something that developed from it [i.e. less habitual energy spent blocking things out], but either way I recommend it :)
try reading it again, and notice how little specific advice is given towards how to cultivate the sort of attention he’s pointing at (maybe his most concrete advice is in the form of a painting of an owl). are you convinced that by trying hard enough the future can belong to you, or that life owes you something? you can create an arbitrary amount of suffering for yourself by living that delusion (or the opposite one, that you can’t influence anything).
the notion expressed in the post is really worth trying, and simple, but hard to explain. one idea: the next time you see something you personally find beautiful (a flower, the sky? the fact that the earth supports you effortlessly?) you could investigate whether you did anything to “deserve” that.
it points out that the bit complexity of the traditional algorithm is actually quadratic. and apparently, restricted to fixed width integers, there is a constant time method.
also, could be marked [2017]
For example, Lean in vscode supports interactive html "widgets": https://youtu.be/8NUBQEZYuis?t=453
(at that timestamp, there's a quick introduction to their typical use at the moment).
lean4 is committed to all sorts of extensibility; here's a demonstration of the new macros: https://twitter.com/derKha/status/1354082976456441861. There have also been several instances of users implementing old lean3 features (for example, the `calc` tactic mode, which has unique syntax for proving (in)equalities) by simply defining new type classes and short macros.
Requiring same size doesn't make it harder; you can take any solution and inflate the dice (take the lcm of all the sizes, duplicate the face numbers).
edit: oops i just double checked my construction and while they give equal go-first probabilities they don't give equal permutation probabilities...