IngoBlechschmid

7 ms·

31.
by IngoBlechschmid 1y ago
> speaking of climate change, global overpopulation kinda has an impact on it! You are right, of course; but just to put some perspective to it: If Thanos-style the population and the CO2 emissions would be cut in half, this would not be
32.
by IngoBlechschmid 2y ago
This circle of ideals seems to be known as: https://en.wikipedia.org/wiki/Cosmological_natural_selection
33.
by IngoBlechschmid 2y ago
Gwern shared an idea how to exploit the strength of current-generation LLMs, despite their weaknesses, for "create your own adventure"-style fiction. https://gwern.net/cyoa Having people vote on AI-generated poten
34.
by IngoBlechschmid 2y ago
> It seems like quite a paradox to build something but to not know how it actually works and yet it works. This doesn't seem to happen very often in classical programming, does it? I agree. Here is a remote example where it exceptio
35.
by IngoBlechschmid 2y ago
You are right, but I would not agree with this appearing "often". I get the impression that the nixpkgs community tries quite hard to truly compile from source even quite complex projects like Firefox and LibreOffice.
36.
by IngoBlechschmid 2y ago
https://en.wikipedia.org/wiki/The_Hundred_Light-Year_Diary By Greg Egan, so highly recommended.
37.
by IngoBlechschmid 2y ago
You mean because the entire known sequence is finite, and every finite sequence occurs in pi infinitely often? This is suspected but currently not yet proven. In fact, we don't even have a proof yet that the digit 7 occurs infinitely o
38.
by IngoBlechschmid 2y ago
Perhaps ironically, despite appearances, the process you propose does not depend on the axiom of choice. This is because we can prove, in the small and generally trusted metatheory PRA, that ZFC is inconsistent if and only if ZF (= ZFC −
39.
by IngoBlechschmid 2y ago
Sorry, I was in a hurry before, the standard approach is exactly what I wanted to refer to with option 1!
40.
by IngoBlechschmid 2y ago
Indeed, and one can give specific metatheorems in this direction: For instance, regarding statements of the form "for all natural numbers x, there is a natural number y such that %", where in "%" no further quantifiers a
41.
by IngoBlechschmid 2y ago
There are three ways to resolve this paradox: 1. Accept that our intuition about volumes is off when dealing with point clouds so weird that they cannot actually be described, but require the axiom of choice to concoct them. 2. Reject the a
42.
by IngoBlechschmid 2y ago
Indeed! For instance, Wikipedia presents a couple of proofs of the irrationality of √2 (including a geometric one). None of these require knowledge of its digits. https://en.wikipedia.org/wiki/Square_root_of_2
43.
by IngoBlechschmid 2y ago
That's a great question, and the answer is by direct inspection that repeating digits cause the number to be rational. For instance, 0.123123123... is checked to be the same as 123/999, a fraction -- hence rational. Similarly, 0.a
44.
by IngoBlechschmid 3y ago
I agree, the axiom of choice disincentives us from striving for more elegant solutions. That said, the axiom of choice is always available in Gödel's sandbox of "constructible sets", and by "Shoenfield absoluteness"
45.
by IngoBlechschmid 3y ago
> To me, ultrafinitism is an intellectual curiosity. Proofs which depend upon the axiom of choice, or a notion of infinity, do not always correspond to algorithms which terminate in finite time. Such results are "useless" to a
46.
by IngoBlechschmid 3y ago
I disagree strongly with this position: * No amount of personal spending decisions can advance systemic changes like better public transport or more careful military funding. These require governmental action. * With our wallet, we can only
47.
by IngoBlechschmid 3y ago
Related: ideas by Gwern to enhance AI dungeons with caching, yielding a novel form of choose-your-own-adventure games. https://gwern.net/cyoa
48.
by IngoBlechschmid 3y ago
This is a great and well-regarded ressource! If you want to experiment with Agda without installing it, you can do so directly in your browser: https://agdapad.quasicoherent.io/
49.
by IngoBlechschmid 3y ago
I like this visualization of the staggering orders of magnitude: https://www.youtube.com/watch?v=QgNDao7m41M
50.
by IngoBlechschmid 3y ago
Good questions! Nowadays, there is indeed a movement towards interoperability between the various proof assistants, one of these bridge-building projects is called Dedukti: https://deducteam.github.io/ It's a challengi
51.
by IngoBlechschmid 3y ago
Two tiny additions: 1. In those proof assistants which don't have the axiom of choice built-in, you can still formalize proofs depending on this axiom by putting it as an extra assumption. One repository using this style which I partic
52.
by IngoBlechschmid 3y ago
Automatic differentiation feels magical. Many compsci people have been captivated by it and wrote introductions, trying to put the technique into a wider perspective. Here is mine, including a "poor man's variant" of automati
53.
by IngoBlechschmid 3y ago
Very nicely polished! Thank you for sharing! For the purposes of teaching Python, I once created something similar---but without the explanations: https://www.speicherleck.de/iblech/zufall-im-browser/index.e...
54.
by IngoBlechschmid 3y ago
Indeed, and nowadays set theorists have rich experiences both in worlds where the Continuum Hypothesis holds and in worlds where it does not. I tried to explain the resulting "multiverse philosophy" (not really related to the idea
55.
by IngoBlechschmid 4y ago
1. Climate is a long-term average. Long-time averages are much simpler to predict than individual outcomes. You cannot predict the result of a coin toss, but you can be reasonably confident that among 1000 tosses there will be between 400 a
56.
by IngoBlechschmid 4y ago
Out of curiosity, why former?
57.
by IngoBlechschmid 4y ago
Fair. (In _Diaspora_ many people are; in _Oceanic_, all.)
58.
by IngoBlechschmid 4y ago
Greg Egan's _Diaspora_ (1997) and _Oceanic_ (1998) come to my mind. Of course not really predating, with what we now recognize as gender fluidity existing for thousands of years, but in any case early texts long before the notion rose
59.
by IngoBlechschmid 4y ago
Indeed, it works as long as the class of labels forms a set instead of a proper class.
60.
by IngoBlechschmid 4y ago
You do not need to worry about the axiom of choice because: (1) Provably so in a very weak (and hence trustworthy) metatheory, assuming the axiom of choice does not result in any new inconsistencies. More precisely: The systems ZFC (Zermelo

More ›