HackerTrans
トップ新着トレンドコメント過去質問紹介求人

butokai

no profile record

コメント

butokai
·13 日前·議論
I am getting 404 right now
butokai
·17 日前·議論
Neither of the two. A proof by contradiction, as other comments have stated, is: assuming not P1, we reach a contradiction; thus P1 must be true. This is equivalent to tertium non datur in classical logic. I’m not sure it’s a valid deduction in your trivalent logic.
butokai
·17 日前·議論
This document misses the point in a way that very commonly arises when mathematicians (as opposed to logicians) discuss proof by contradiction. The examples in this document all revolve around assuming a fact, showing that it would lead to an absurd, and thus establishing that that fact can’t be the case: there is no rational equal to sqrt(2), there is no finite listing of all the primes. They are not using proof by contradiction at all, and on the contrary these proof are fully constructive: if one where to give us what they believe is a finite list of all the primes, the proofs gives us a method to construct a new prime.

Proof by contradiction, on the other side, deems that we derive a contradiction from the assumption that a statement does not hold. Then, by contradiction, we may state that is true because it is impossible for it to be false.

This is why it is rejected by the intuitionists and constructivists: there is no way to extract an explicit procedure from such a proof, since it only states that what can’t be false must me true.
butokai
·先月·議論
Do you think there will still be an incentive to release weights in that scenario? Everyone will have models only if there continue to be companies releasing weights.
butokai
·2 か月前·議論
I remember trying an iPhone 12 in 2020 and feeling it was so fast that no phone task would ever be able to use all that power. Definitely not my current experience on my now old iPhone 12. A lot of it can be attributed to ever increasing ram usage by web pages, but that doesn’t seem to be all.
butokai
·3 か月前·議論
Same for me! It took me a while staring at the article and wondering why "browser" was mentioned so many times, to realize it was not Android
butokai
·3 か月前·議論
That's what I was thinking, but the phrasing seems to imply that he did update to 26.4.1? Not sure how that was possible.
butokai
·4 か月前·議論
This setup feels cumbersome, since you also have to manually track which items you have read. Kobo seems to offer better features in this sense (better than a jail broken kindle), however I like the build of my Kindle Oasis 2 too much.
butokai
·4 か月前·議論
As an Italian living in another EU country, I always thought that the amount of (broken) bureaucracy of Italy was not particularly worse. However this story comes after a couple more I heard this week, in a line of absurd practice possibly due to absurd regulations.
butokai
·5 か月前·議論
Just a couple of hours ago I was thinking about this project from some time ago doing the same thing: https://github.com/evmar/retrowin32

I wondered how much of this could be done with an LLM agent, and here we have the answer
butokai
·5 か月前·議論
Funnily enough, when programming with agents in statically typed languages I always find myself in need of reminding the agent to check for type errors from the LSP. Seems like it's something they're not so fond of.
butokai
·9 か月前·議論
This is a viewpoint commonly held by students who were exposed to imperative programming before having any class in maths. However it shouldn't survive long after that.
butokai
·11 か月前·議論
I just moved to macOS for the first time, and my only way to adapt to its multi-tasking has been keeping exactly one window per open application, never zero or more than one. The fact that Finder can't be treated like that is a real pain. I will focus on it essentially randomly, and it will disrupt my intended interaction.

I don't get the reasoning behind the zero-window cmd-tab interaction, but if it is there I guess that there's a reason behind it?