tbt

Sigh, thanks for letting me know. Ok since this is the ~third time someone has said this, I'll try to figure out a convenient solution (I guess hosting images on github?). Just FYI a VPN should let you see imgur images.

Oh sorry that was a joke. (Though you could teach that in kindergarten.) When I was in undergrad I had the privilege of taking Laszlo Babai's combinatorics class. I don't recall exactly how he phrased it, but he would say things like "As everyone learns in kindergarten, the powerset of [n] has size 2^n.".

Ohhh, oops, good point, thanks.

Yeah I use imgur, which I've heard is somehow blocked in the UK. The US should work. Maybe I'll try to figure out fallback images and double-host on github, if that's a thing.

Thanks. Yeah I'm happy it at least exists somewhere.

Regexression

Idiocracy: https://www.youtube.com/watch?v=sVyRkl5qNb8

Does anyone know any writeups that describe how someone solved a difficult problem they couldn't previously solve, using a note-taking app?

It rarely helps with learning vs. natural counterfactuals. It harms by socializing kids to not believe that their own curiosity is hopeworthy.

See John Taylor Gatto's work.

Instead of inefficient spending for large, programmed classes, you should have daycare/day supervision with lots of resources (books, internet, age-appropriate tinker equipment like electronics and tools and so on, microscopes, telescopes, a few adults on hand who are experts in whatever topic to help kids get traction / navigate), more free-rangness, less authoritarianness, more mastery learning, more apprenticeship.

School rarely helps with learning and almost always harms learning. If you're still sending your kids to school, be mindful that you're doing that for reasons other than to help them learn.

I had a math question that had some free parameters, making it a sort of question machine, giving one question for each setting of the parameters. It was hard to keep track of my thoughts and partial answers about the question-family, so I made a multi-dimensional spreadsheet in vim, so I could see at a glance which questions I'd answered or not.

More details in this blog post: https://tsvibt.blogspot.com/2022/06/multisheets-multi-dimens...

The browser could give the user a unique popup style (colored borders, etc.). As long as that info is hidden, this attack would have only a tiny chance of succeeding.

Have you seen gwern's essay on computational complexity arguments about AI? https://www.gwern.net/Complexity%20vs%20AI

>Self-trust seems like a problem on paper, but the reality is that normal mathematics uses very few universes.

Self-trust (broadly construed) is interesting to me because it seems relevant to designing goal-based agents that are "stable", in the sense that they trust that future versions of themselves will have accurate beliefs (and therefore don't have an incentive to mess around with their systems for forming beliefs). If we try to formalize this intuition with "beliefs" as theorems proven by a formal system, we run into reflection problems; having your theorem prover assert that it will keep outputting only true statements feels awfully close to asserting its own soundness. So even if your agent can perform all the usual mathematical reasoning it needs, it still can't do all the useful reasoning about itself (it would need another large cardinal... and then another...).

The self-trust property in the paper says that it's possible to "learn from experience" that your future self is probably going to have pretty good beliefs. Specifically, a logical inductor P_n learns (roughly speaking) that "if P_f(n) thinks Phi is likely, then Phi is likely", where f(n) can be a fast-growing computable function. That is, on day n, P_n believes a sort of "probabilistic soundness" condition for its future self P_f(n). This is weaker than full soundness in at least two ways, but it is fully "reflective" in the sense that P believes this of itself.

[ For some work formalizing a reflection principle in HOL, see https://intelligence.org/files/ProofProducingReflection.pdf ]

Yep, that's the idea :)

This is in the vein of "prediction using ensembles of experts" methods such as SI, with a twist that the experts are traders, not forecasters; they don't have to have opinions on everything the logical inductor has to predict, the traders just have to point out particular ways that the logical inductor is being silly (and then the logical inductor corrects those problems).

Yeah. It's still surprising to me, though; P_n can predict extremely long-running computations, even ones with a much longer runtime than P_n, at least as well as any quickly computable "pattern". (The algorithm in the paper uses a (roughly) double-exponential-time algorithm to predict arbitrarily long-running programs, in a way that can't be improved upon by any polytime computable method.)

> This allows you to state and show meta theorems "for all (small) types", by quantifying over a universe.

As you say, this isn't quite self-trust. Another natural move is to relax the criterion of self-trust away from "it proves itself consistent" (impossible by incompleteness) towards "it assigns high probability that it has good beliefs". (Formalizations of this are in the paper.)

> At the moment I'm just confused what the problem is

In short, it would be nice to have a model of "good reasoning under deductive limitation", where "good reasoning" means something like "has accurate beliefs about all questions of interest" (for example, facts about the outputs of long-running computations), and where "deductive limitation" rules out the reasoning process "just wait for your theorem prover to decide the question".

Examples of long-running computations that are hard to compute exactly, but that we can sometimes still have reasonable beliefs about: optimal moves in chess, go, etc.; the accuracy of some ML system after a given training regimen; a weather-forecasting program that runs a gigantic series of simulations; and so on.

This is a good point. I think it'd be pretty interesting and useful to get a better grasp on when/whether/how a system can reason about itself as embedded in the world in a sane way.

This is right, but perhaps misleading; most of the properties are "asymptotic", meaning that they may take an extremely long time to hold, but they hold at finite times. For example, "provability induction" says that if you have a (polytime computable) sequence of sentences phi_n, all of which happen to be provable (possibly with fast-growing proof lengths), then P_n(phi_n) limits to 1. This means that on day n the logical inductor P is confident of phi_n, even though phi_n may take much longer than n steps to prove.

The universal semimeasure is "computably approximable from below", aka (lower) semicomputable, meaning that you can computably list out all the rational numbers below a given value assigned by the measure. The probabilities assigned by a logical inductor are computably approximable reals, which (confusingly) is weaker than lower semicomputable; it just means that you can compute a sequence of rationals that converges to the real, with a possibly uncomputable convergence rate.