All of Smaug123's Comments + Replies

Notes from second meeting

Answer to exercise "What's the sentence you get from the diagonal lemma, L iff 'L has length less-than-or-equal-to 1000'?": len("replace('len(x) <= 1000", 'x' -> "replace('len(x) <= 1000', 'x' -> x)")") <= 1000. I think.

We went through the Smullyan paper and got up to the moment before "The Stability Predicament". The point of the paper turns out to be "if we interpret the box modality as 'belief', then a bunch of English sentences sound weird". The real moral of the paper is that it's awfully hard to be a knight or ... (read more)

Date and time of second meeting

Friday 23rd August, 7pm. Location: Notes, St Martin's Lane (Trafalgar Square), open til 9pm. I'll have a crew cut and will be wearing a Doge t-shirt.

Agenda: I'd like to understand Smullyan's paper about Löbian reasoning on the island where people either always tell the truth or always lie. See the previous session's notes for what we've done so far (I've summarised with a lot of jargon; I don't expect attendees to be fluent with jargon, so don't be too daunted by the summary.)

Bring writing implements and paper if you possibly... (read more)

Notes from first meeting

Summary: we haven't actually got to the meat of Löb's theorem yet.

We went over:

  • first-order logic
  • enough model theory to observe that "truth" is a property of a sentence applied to a model, whereas "provability" is a property of a sentence applied to a theory
  • mentioned Gödel's completeness theorem (that "provable" = "true in all models")
  • mentioned the Löwenheim-Skolem theorems which guarantee that there are nonstandard models of Peano arithmetic (in fact, nonstandard models of arbitrarily large cardinality), and handwaved what the small
... (read more)

I am just about to put up my notes from the first session and to announce the next one! I'm intending Friday 23rd, again at Notes Trafalgar Square, 7pm.

I organised the first one at too short notice, so there were just two of us there, but there are several more people with "yes but give me more notice" status. Since there were only two of us, we went over groundwork in advance of the theorem itself. Still plenty of time for people to come in at the beginning!

OK, I'm finally both not on holiday and not on the support rota at work.

Date and time of first meeting

Friday 16th August, 7pm. Location: Notes, St Martin's Lane (Trafalgar Square), should be open til 9pm. I'll have a crew cut and will be wearing a Doge t-shirt. If it all goes wrong, in an emergency we can go and have nibbles at Prezzo instead.

Agenda: don't know how far we'll get, but I ambitiously hope we can fully grok Löb's theorem itself by the end of this. You should first refresh your knowledge of first-order logic and Peano arithmetic if you need to.... (read more)

1kapslock
I didn't check my notifications frequently enough to see this. How far did you get into the theorem, and will there be another session?
2philh
Ah, I can sometimes make fridays but not tomorrow. Hope it goes well.

See https://doodle.com/meeting/participate/id/epXrAqme to vote for times and places! Hack: I'm using "midday" to mean "7-9pm, but remote rather than in person". I intend meetings to be weekly until we (I) run out of joy or things to talk about. Up front I'm leaning fairly strongly towards in-person (e.g. because I expect a bunch of shared whiteboarding stuff that I've always found a bit painful over e.g. Jamboard).

@the gears to ascension @LukasM 

2the gears to ascension
Well, I'm not going to be in london any time soon.

Post for people to register time zone preference. No guarantees that I won't end up just saying "urgh organisational tsouris is raising the activation energy too high, so this group is happening in-person in London after all", but if we do end up remote, I'll consider time zones in this thread!

I vote for a time compatible with the evening of London UK, or a time compatible with the afternoon on Sundays. I declare the cadence to be weekly by default.

2the gears to ascension
I suggest any time during the intersection of london and eastern time, ie london evening. (I'm not in either, but that intersection is a reliable win for organizing small international online social events, in my experience)

By the way, as an extremely verbally-fluent nondyslexic person who was also an excellent choral singer, I can confirm the superpowers of singing versus talking. For example:

  • I can recite some Maori, Zulu, and a bunch of Hebrew, with only a vague idea what it means (I'm sure I once knew), because of a singing it in a variety of songs. (And like many singers I can recite large tracts of Christian liturgy in Latin; in fact to recite it in English I usually have to translate on the fly from Latin.)
  • I memorised about 140 digits of pi just by having Hard 'n' Phirm
... (read more)
3Shoshannah Tekofsky
oh huh ... It hadn't occurred to me to use it for memorization. I should try that, considering I think I have subpar memory for non-narrative/non-logical information like strings of numbers. Good point! Conversely, I think I have above average memory for narrative and logically coherent information like how things work or events that happened in the past. It feels like that type of information has a ton of "hooks" such that I can use one of a dozen of them to recall the entire package, while a string of numbers has no hooks. It's like someone is asking me to repeat white noise. But phone numbers and codes and what not are that. Let alone trying to keep track of numbers on something like a graphics card or processor (I gave up).
1Vaughn Papenhausen
Yup. This is how I learned German: found some music I liked and learned to sing it. I haven't learned much Japanese, but there's a bunch of songs I can sing (and know the basic meaning of) even though I couldn't have a basic conversation or use any of those words in other contexts

If you have the power to change the Google form, by the way, one of its questions is "What dose did you take (in mg)? 0.5, 1, 1.5, 2+"

Presumably this should read "(in g)", and it would also help if it were explicitly stated as being "per day".

This isn't necessarily something you have to be tricked by a third party into. Be more Gwern! If there are two brands of cola you've not tried before, one stevia and one not, you can do a blinded trial by decanting them or similar. It'll certainly be easier with a third party, but one could do this solo.

There's an analogy with the notion of "toil" which is popular in the Site Reliability Engineering subfield of software engineering. Toil in this context is work which is necessary to keep the lights on, but which doesn't actually improve anything. In some sense, the job of an SRE is to reduce toil; they must certainly be psychologically able to deal with it, because it's the stuff with which they work! I'll just talk a bit about it here in a fairly undirected way, in case any of it gives you ideas. The SRE Handbook is well worth reading if you're a softwar... (read more)

2MondSemmel
I love hearing about the overlap between personal life stuff and concepts from technical fields. So thanks a lot for this comment! Another instance of this topic is the advice from the book Algorithms to Live By. Also, I'd love to hear more about this stuff. Furthermore, I think the general theme of "general-purpose advice based on what I learned in my work" is very fruitful for blog posts, including LW posts.

It would be nice to have example GPT4 outputs for each demonstrating the wrongness, because I tried "Continue the sequences: 5, 8, 13," expecting the answer 21, and for me it did indeed explain along the lines "21, because Fibonacci". As you say, this dataset is inherently unstable over time, so it would be nice to snapshot it. (One obvious way would be to convert from a list of strings to a dictionary of `{ "prompt": ["response1", "response2", …] }`; the current schema injects into this by setting all those lists to be empty.)

suffering is bad because anyone who suffering is objectively in negative state of being.

I believe this sentence reifies a thought that contains either a type error or a circular definition. I could tell you which if you tabooed the words "suffering" and "negative state of being", but as it stands, your actual belief is so unclear as to be impossible to discuss. I suspect the main problem is that something being objectively true does not mean anyone has to care about it. More concretely, is the problem with psychopaths really that they're just not smart enough to know that people don't want to be in pain?

By the way, you're making an awful lot of extremely strong and very common points with no evidence here ("ChaosGPT is aligned", "we know how to ensure alignment", "the AI understanding that you don't want it to destroy humanity implies that it will not want to destroy humanity", "the AI will refuse to cooperate with people who have ill intentions", "a system that optimises a loss function and approximates a data generation function will highly value human life by default", "a slight misalignment is far from doomsday", "an entity that is built to maximise s... (read more)

A moderator has deactivated replies on this comment

(Or more concretely, Grand Central Station wasn't a Schelling point in New York before it was built. Before that time, presumably there were different Schelling points.)

1Martin Randall
I think we can distinguish between humans changing the environment in a way that happens to create a Schelling point, vs communicating to create a coordination strategy. Wikipedia at least agrees with TAG's definition.

Fittingly, I… don't think those words actually identify sazen :P I claim that "the thing you get if you do not take inferential distance into account" for most people would be baffled non-comprehension, not active misunderstanding.

3Gunnar_Zarncke
Hm, yes, I can see that would happen at higher levels of inferential distance. But for small distance wouldn't you say it's close?

Wonderful, thanks! Recording the quote for posterity:

Nothing can be soundly understood 
If daylight itself needs proof.

(Imam al-Haddad⁠, The Sublime Treasures)

Indeed, this is what I use. It feels much more natural to me in the following case, where obviously our statement is not a question:

Dr Johnson kicked a large rock, and said, as his foot rebounded, "Do I refute it thus?".

And "obviously" the full stop should go outside, because of:

Dr Johnson kicked a large rock, and said, as his foot rebounded, "Do I refute it thus?", howling with pain.

And there's nothing special about a question mark, so this rule should be identical if a full stop is substituted.

4Gunnar_Zarncke
That's what I do. I know it is wrong but honestly, I don't care. It just makes more sense.

I will pick a rather large nit: "for example a web server definitely doesn't halt" is true, but for this to be surprising or interesting or a problem for Turing reasons, it just means you are modelling it incorrectly. Agda solves this using corecursion, and the idea is to use a data type that represents a computation that provably never halts. Think infinite streams, defined as "an infinite stream is a pair, $S_0 = (x, S_1)$, where $S_1$ is an infinite stream". This data type will provably keep producing values forever (it is "productive"), and that's what you want for a web server.

3Yair Halberstadt
That's fair. I think a better way of putting my point is, can we express the particular behaviors I'm interested in proving, and only have the compiler care about those, rather than checking everything it might be interested in.

I'm pretty sure it's not schools, unless private schools somehow have a massive impact. The case rates were already dropping on July 21st, which is presumably a couple of days after The Event anyway; the summer holidays for state schools (i.e. the vast majority of children) started on the 25th.

Irrelevant nit: the archaic second-person singular of "do" is "dost", as in "dost thou not know". "Doth" is the third-person form, as in "the lady doth protest too much".

For some reason I can't find any relevant hits with Google, but I've heard "support vs advice" described as "sympathy or fascism" before. "I want to moan at you" vs "I want you to take over and solve my problem".

2abramdemski
Haha, what a terrible choice of descriptors! I mean, it gets across the point of view of the "sympathy" side, which is arguably more important than getting across the other side (since I've more often heard about the error of giving advice than the opposite), but... how unsympathetic ;p

For some years now I have had a Panasonic breadmaker, model SD-ZB2512. It takes less than five minutes in the evening, generating no mess and no washing up (if you use olive oil instead of butter, so as to avoid generating a fatty knife), and you can have hot fresh bread ready-baked as you wake up. The only downside to bread made this way is that you have to slice it. It tastes dramatically better than all but the most expensive shop-bought bread, and the ingredients store in a cupboard for literally months so it's even highly pandemic-proof. Bread that is... (read more)

(Posting this in a spirit of self-congratulation: I wrote up a spiel about what I found confusing, and then realised that I'm confused on a much more fundamental level about the nature of the various explanations and how they relate to each other, and am now going back to reread the various sources rather than writing something unhelpfully confusing about a confused confusion.)

1Ben Pace
smug smaug :)

Strong +1 to the idea; I'll be on a different team, but I strongly encourage people to give it a try. I think Hunt 2019 was quite possibly the most fun I have ever had.

My immediate reaction is that I remember hating it very much at school when a teacher punished the entire class for the transgression of an unidentifiable person!

4johnswentworth
Same! I thought about putting that in as an example, but didn't end up using it.

Nitpick: I think there's a minor transcription error, in that "biological-esque risk" should read "biological X-risk".

Answer by Smaug123130

You're thinking of "Glomarisation" (https://en.wikipedia.org/wiki/Glomarization).

See, for example, https://www.lesswrong.com/posts/xdwbX9pFEr7Pomaxv/meta-honesty-firming-up-honesty-around-its-edge-cases and https://www.lesswrong.com/posts/bP5sbhARMSKiDiq7r/consistent-glomarization-should-be-feasible.

1[anonymous]
Thank you!

I'm a big believer in "the types should constrain the semantics of my program so hard that there is only one possible program I could write, and it is correct". Of course we have to sacrifice some safety for speed of programming; for many domains, being 80% sure that a feature is correct in 95% of the possible use cases is good enough to ship it. But in fact I find that I code *faster* with a type system, because it forces most of the thinking to happen at the level of the problem domain (where it's easy to think, because it's clos... (read more)

I believe the world is this way because of the following two facts:

  • monads are very hard to get your head into;
  • monads are extremely simple conceptually.

This means that everyone spends a long time thinking about monads from lots of different angles, and then one day an individual just happens to grok monads while reading their fiftieth tutorial, and so they believe that this fiftieth tutorial is The One, and the particular way they were thinking about monads at the time of the epiphany is The Way. So they write yet another tutorial about how Monads Are Reall... (read more)

1lc
You are very funny and have convinced me maybe possibly to try haskell again. But only maybe.

I'm interested in your comment about "using dynamic-untyped rather than well-typed because it helps you not worry about your own intelligence". I use well-typed languages religiously precisely for that reason: I'm not smart enough to program in an untyped language without making far too many mistakes, and the type system protects me from my idiocy.

1lc
You misunderstand me. I don't use the simpler products because otherwise I worry about my own intelligence. What I found was that in order to protect my ego, and because I thought I was smarter than I was, I consistently used software engineering tools and platforms that were complicated to the point of hurting my ability to program. I will remove Go from the above post because I think it doesn't fit; I dislike Go's genericless type system because it constrains my programs and not because I'm thinking about it all the time. With regard to "well-typed" programming languages, the problem isn't that they don't help me write more correct code - they do. The problem is that they make me think about types to a degree that's often unnecessary or irrelevant to solving the problem at hand, and while performing exploratory programming I have to deal with these type algebras that are a context switch from my ML or infrastructure problems. Most bugs are problems with semantics and not syntax, so normally thinking very hard about types turns out to be wasted effort in the long run.
1Quentin Crain
Wrt typing, we have: * Strict/strong: c, go, java, erlang * Strict/weak: doesn't exist right? * Dynamic/strong: python, elixir * Dynamic/weak: Perl I prefer dynamic and don't particularly care about strong/weak since generally my programs don't do what I want because they are semantically wrong, not syntactically.

You can buy good tomatoes (in the UK); they're just a bit expensive. Cheap tomatoes are nasty, but nice tomatoes are widely available; I get them from a company called Isle of Wight Tomatoes, and they're on Ocado.

I stopped taking the book seriously when I reached Walker's suggestion that teenagers might have a sleep cycle offset from adults because "wise Mother Nature" was giving them the chance to develop independence from the tribe, in a group of their peers, and that this was an important stage in societal development of a human.

If one *must* find an evo-psych explanation for this phenomenon, surely "we need people guarding the camp at more hours of the day" is simpler and less ridiculously tenuous. (Though this still has precisely the same "I could have explained anything with this" flavour that most popular evo-psych does.)

1guzey
(removed this comment)
Answer by Smaug12330

I've had experiences ranging from "great" to "terrible" when pairing. It's worked best for me when I'm paired with someone whose skills are complementary to mine. Concretely: I'm very much about rigour, type-safety, correctness; the person I have in mind here is a wizard at intuiting algorithms. The combination worked extremely well: the pairer generated algorithms, and I (at the keyboard) cast them into safe/correct forms.

However, when paired with someone who eclipses me in almost every dimension, I ended up feeling... (read more)

I started Anki-ing everything. Previously, I've used Anki for very specific purposes (e.g. "learn the London Underground network" or "learn all the capitals of the world"). New decks this month, though, include "Jokes", "Legal Systems Very Different From Ours", "Tao Te Ching", and "Logical Induction". I'm pretty optimistic that "read something really worthwhile, Anki it up" is becoming a habit.

A formative experience in my attitude to magic was when I saw an excellent sleight-of-hand magician performing to my small group of friends (waiting in a line for an event). He was very convincing and great fun; but there was a moment in the middle of his series of tricks when my attention was caught by something else in the distance. When I looked back after five seconds of distraction, he was mid-trick; and I saw him matter-of-factly take a foam ball from his hand, put it into his pocket, and then open his hand to reveal no foam balls - to general astoni... (read more)

Thanks very much for this! I've written a lot of stuff on there (I'm the Patrick Stevens whose name is splatted all over the screenshot). I asked them a year ago (ish) whether I could have a data dump, and they said it was Too Difficult; and I didn't bother scraping it myself. I'm glad you actually went and did something about it!

On introductory non-standard analysis, Goldblatt's "Lectures on the hyperreals" from the Graduate Texts in Mathematics series. Goldblatt introduces the hyperreals using an ultrapower, then explores analysis and some rather complicated applications like Lebesgue measure.

Goldblatt is preferred to Robinson's "Non-standard analysis", which is highly in-depth about the specific logical constructions; Goldblatt doesn't waste too much time on that, but constructs a model, proves some stuff in it, then generalises quite early. Also preferred to... (read more)

True, though the decision of who is most cost-effective does remain for you to decide.

It's more of a tactic to make sure people don't think "hey, another crackpot organisation" if they haven't already heard about them. I'm hoping to raise GWWC to the level of "worth investigating for myself" in this post.

I do something similar. I consistently massively underestimate the inferential gaps when I'm talking about these things, and end up spending half an hour talking about tangential stuff the Sequences explain better and faster.

5MathiasZaman
Since I mostly communicate in Dutch when in meatspace, I find myself rarely using terms directly from Less Wrong (because good translations don't always come to mind). Of course, this isn't exactly a lifehack, since you wouldn't expect most people to move to a different language zone for a minor benefit.
0Gunnar_Zarncke
Same with me. Except pointing to LW or the sequences doesn't help.

I'd frame it as "Nick Bostrom needs Jeeves. Are you Jeeves?" (After P.G. Wodehouse's Jeeves and Wooster.)

4gjm
Jeeves is drastically more competent than Wooster at pretty much everything. That may not be the image you want to call up.