💾 Archived View for gemlog.blue › users › jiaming › 1629826298.gmi captured on 2022-04-09 at 13:53:08. Gemini links have been rewritten to link to archived content
-=-=-=-=-=-=-
24/08/2021 (things i learned)
- unrestricted conversations with strangers are refreshing
- regarding christianity, most people dont just convert based on ideology, they know real people who seriously believes in it, i hypothesise that that lays the foundation for conversion
- baseline views to set conversation/reading, like take this as an assumption for the moment even if you dont believe in it
- "my political ideology is science" xD
- ugh so obvious, the main reason companies support open source is because they only want to support DEVELOPER TOOLING. It makes complete sense for them then: Additional experience filter, cheaper outsourced production tools, devs are the only people in the world who even understand the issue. In the case of big companies like google, they support nondev tools cuz they want to snatch them up early; for smaller companies, more sincere imo, also cuz their devs really want to.
i shuold be studying fluid mechanics ugh
- teaching vectors: Imagine at first you have nothing except the holy dot. The rule is you can only draw (however many) straight lines from the dot to anywhere else. If you were an evil crazy genius mathematician, what super ultra complex mathematical theorems would you invent? You can try to break the rules, but ill explain whether its valid or not
- PETER AND JANE? Bottom floor at/past corridor facing playground. Ceiling wayy taller (though space is a little contradictory) maybe its the new handsoap smell? very foreign to me but maybe smelled before when young
- heh 10% for practical quiz, 100% for preworkshop
- MC interview with "fundamental universal graph theory" colonizer? haih... but lets watch. understand where crankery meets new horizons
- features i dream to have on tusky: keep at least some posts, notifications and my personal timeline locally
- features i dream to have on newpipe: export links/metadata in plain text and more advanced search filtering
- just because someone sides your argument for one thing doesnt mean that person is any more on your side than your opponents
- lmfao so many monash confession duplicates
- mimetypes lack standards
- tokyo paralympics.. no one talked about it until it started
- just setting up lean 4 will be a big task for me in itself, but i think i'll learn alot (fuck nvm it's all elan... buh-ring) oop i forgot about emacs, but its doable with the internet's help
- damn the porting effort from lean3 to lean4 is incredible... im just in awe (and i LOVE Lean 4 so much from the first looks of it) holy shit im in love with lean again... coq is like ancient beast haha
- lean has an official independent *reference* typechecker! how tf did i not know about this haha https://github.com/leanprover/tc
- fixing other people's youtube subs is NOT worthwhile AT ALL, or maybe that stupid online vtt-srt converter just sucks
- wow lean really can make u feel competent and incompetent at the same time...
- even toots can be easily misunderstood
- wow lean is so mysterious... and so well made? i dont like it but im amazed
- hahahah lean4-mode doesnt have a goal window yet?? cool cool, executing it will be fine... hopefully
- lean4's cool, not magical but super intriguing
- file://~/Desktop/Lean4/Resources/leanprover.github.io/lean4/doc/do.html