Xcelerate

Lately I’ve been thinking I might have better odds making a straight shot for ASI on my own over practicing and rehearsing the material that needs to be presented almost perfectly in the AI interviews. I’ve worked at FANG in ML / applied research for almost a decade but still can’t even get a screening interview at the top places without asking someone I know for a referral. And I really hate bugging former coworkers for referrals. Normally end up procrastinating on reaching out until the job postings just disappear haha.

I feel like there’s an interesting follow-up problem which is: what’s the shortest possible proof of FLT in ZFC (or perhaps even a weaker theory like PA or EFA since it’s a Π^0_1 sentence)?

Would love to know whether (in principle obviously) the shortest proof of FLT actually could fit in a notebook margin. Since we have an upper bound, only a finite number of proof candidates to check to find the lower bound :)

I could see this. For certain personality archetypes, there are particular topics, terms, and phrases that for whatever reason ChatGPT seems to constantly direct the dialogue flow toward: "recursive", "compression", "universal". I was interested in computability theory way before 2022, but I noticed that these (and similar) terms kept appearing far more often than I would expect to due chance alone, even in unrelated queries.

Started searching and found news articles talking about LLM-induced psychosis or forum posts about people experiencing derealization. Almost all of these articles or posts included that word: "recursive". I suspect those with certain personality disorders (STPD or ScPD) may be particularly susceptible to this phenomenon. Combine eccentric, unusual, or obsessive thinking with a tool that continually reflects and confirms what you're saying right back at you, and that's a recipe for disaster.

Thanks for sharing! I didn’t think about all of the intermediate steps that might be difficult to encode, but that makes sense.

I’m not up-to-date on how advanced proof assistants have become, but are we not nearing the point where serious attempts at proving P vs NP can be automatically validated (or not) by a widely vetted collection of Lean libraries?

The P vs NP problem is expressible as the question of whether a specific Π_2 sentence is true or not (more specifically, whether a particular base theory proves the sentence or its negation). Unlike problems involving higher order set theory or analytical mathematics, I would think any claimed proof of a relatively short arithmetical sentence shouldn’t be too difficult to write up formally for Lean (although I suppose Fermat’s Last Theorem isn’t quite there either, but my understanding is we’re getting closer to having a formal version of it).

The impact of this would be that journals could publicly post which specific sentences they consider to represent various famous open problems, and a prerequisite to review is that all purported proofs require a formal version that automatically Lean-validates. This would nix the whole crank issue.

Then again, I may be way off base with how close we are to achieving something like I’ve described. My impression is that this goal seems about 5 years away for “arithmetical” mathematics, but someone better in the know feel free to correct me.

It’s gotten absurd. I’ll easily pay 10x the regular price of some object if I’m confident it will last a very long time and I won’t have to think about it anymore. I’ve replaced all the crappy LED bulbs in my house with Yuji Sunwave brand. I’ve not had a single bulb flicker or go out in years now, and the quality of the light is superb (i.e. more akin to what everyone used to have with incandescent bulbs). I bought a Control Freak induction cooktop in 2018. The whole family uses it far more than the cheap gas range that came with the house and is a pain to clean. Similarly, I replaced all the Food Network brand pots and pans I had in college that were chipping paint and rusting with Demeyere versions. Not a single problem since.

And to your point, I’ve probably gone through six clothes drying racks by now that all break down after a short time. I have yet to find a high-quality one.

It sounds expensive, but I suspect that in the long-term, the approach of buying higher quality up front ultimately ends up cheaper in terms of time and replacement costs. I’ve debated replacing some home appliances with commercial or restaurant versions, but there are some notable tradeoffs with that unfortunately, as the purpose of the appliance becomes somewhat different than a home use case.

Of course this strategy is all well and good if you can foot the initial high cost of the products, which many people cannot on the typical family income. There’s been a lot written about how those of lower income are often taken advantage of in this way—they end up paying a higher “lifetime cost” for lower quality products and service, because the system attempts to produce the minimum viable affordable product, which then sets the bar for the “new normal”.

Edit: I wrote my comment a bit too early before finishing the whole article. I'll leave my comment below, but it's actually not very closely related to the topic at hand or the author's paper.

I agree with the gist of the article (which IMO is basically that universal computation is universal regardless of how you perform it), but there are two big issues that prevent this observation from helping us in a practical sense:

1. Not all models are equally efficient. We already have many methods to perform universal search (e.g., Levin's, Hutter's, and Schmidhuber's versions), but they are painfully slow despite being optimal in a narrow sense that doesn't extrapolate well to real world performance.

2. Solomonoff induction is only optimal for infinite data (i.e., it can be used to create a predictor that asymptotically dominates any other algorithmic predictor). As far as I can tell, the problem remains totally unsolved for finite data, due to the additive constant that results from the question: which universal model of computation should be applied to finite data? You can easily construct a Turing machine that is universal and perfectly reproduces the training data, yet nevertheless dramatically fails to generalize. No one has made a strong case for any specific natural prior over universal Turing machines (and if you try to define some measure to quantify the "size" of a Turing machine you realize this method starts to fail once the number of transition tables becomes large enough to start exhibiting redundancy).

I find the current VC/billionaire strategy a bit odd and suboptimal. If we consider the current search for AGI as something like a multi-armed bandit seeking to identify “valuable researchers”, the industry is way over-indexing on the exploitation side of the exploitation/exploration trade-off.

If I had billions to throw around, instead of siphoning large amounts of it to a relatively small number of people, I would instead attempt to incubate new ideas across a very large base of generally smart people across interdisciplinary backgrounds. Give anyone who shows genuine interest some amount of compute resources to test their ideas in exchange for X% of the payoff should their approach lead to some step function improvement in capability. The current “AI talent war” is very different than sports, because unlike a star tennis player, it’s not clear at all whose novel approach to machine learning is ultimately going to pay off the most.

I don’t understand your post. You’re linking to a discussion about the same conjecture I mentioned in another comment 11 hours prior to your comment. Did you mean to link something else?

Yeah, I’m quite familiar with Friedman’s work. I mentioned him and his Grand Conjecture in another comment.

> This ignores the fact that it is not so easy to find natural interesting statements that are independent of ZFC.

I’m not ignoring this fact—just observing that the sheer difficulty of the task seems to have encouraged mathematicians to pursue other areas of work beside foundational topics, which is a bit unfortunate in my opinion.

> obviously we could simply take every true sentence of Peano arithmetic as an axiom to obtain a consistent and complete system

If you’re talking about every true sentence in the language of PA, then not all such sentences are derivable via the theory of PA. If you are talking about the theorems of PA, then these are missing an infinite number of true statements in the language of PA.

Harvey Friedman’s “grand conjecture” is that virtually every theorem that working mathematicians actually publish can already be proved in Elementary Function Arithmetic (much weaker than PA in fact). So the majority of mathematicians are not pushing the boundaries of the existing foundational theories of mathematics, although there is certainly plenty of activity regardless.

Right, Hilbert’s goal was (loosely speaking) to “find a finitely describable formal system” sufficient to “capture all truths”. When Gödel showed that can’t be done, that shouldn’t imply we just stop with the best theory we have so far and call it a day—it means there are an infinite number of more powerful theories (with necessarily longer minimal descriptions) waiting to be discovered.

In fact, both Gödel and Turing worked on this problem quite a bit. Gödel thought we might be able to find some sort of “meta-principle” that could guide us toward discovering an ever increasing hierarchy of more powerful axioms, and Turing’s work on ordinal progressions followed exactly this line of thinking as well. Feferman’s completeness theorem even showed that all arithmetical truths could be discovered via an infinite process. (Now of course this process is not finitely axiomatizable, but one can certainly extract some useful finite axioms out of it — the strength of PA after all is equivalent to the recursive iteration up to ε_0 of ‘Q_{n+1} = Q_n + Q_n is consistent’ where Q_0 is Robinson arithmetic).

At some point big numbers become much more about the consistency strength of formal systems than “large quantities”.

I.e., how well can a system fake being inconsistent before that fact it discovered? An inconsistent system faking consistency via BB(3) will be “found out” much quicker than a system faking consistency via BB(6). (What I mean by faking consistency is claiming that all programs that run longer than BB(n) steps for some n never halt.)

It boggles my mind that we ever thought a small amount of text that fits comfortably on a napkin (the axioms of ZFC) would ever be “good enough” to capture the arithmetic truths or approximate those aspects of physical reality that are primarily relevant to the endeavors of humanity. That the behavior of a six state Turing machine might be unpredictable via a few lines of text does not surprise me in the slightest.

As soon as Gödel published his first incompleteness theorem, I would have thought the entire field of mathematics would have gone full throttle on trying to find more axioms. Instead, over the almost century since then, Gödel’s work has been treated more as an odd fact largely confined to niche foundational studies rather than any sort of mainstream program (I’m aware of Feferman, Friedman, etc., but my point is there is significantly less research in this area compared to most other topics in mathematics).

Haha, I like to joke that I reached peak intellectual capacity around 26 and peak emotional maturity around 14 and both have been dropping from their peak since then.

Do wide events really have to take up this much space? I mean, observability is to a large degree basically a sampling problem where the goal is to maximize the ability to reconstruct the state of the environment at a given time using a minimal amount of storage. You can accomplish that by either reducing the number of samples taken or by improving your compression capability.

For the latter, I have a very hard time believing we’ve squeezed most of the juice out of compression already. Surely there’s an absolutely massive amount of low-rank structure in all that redundant data. Yeah, I know these companies already use inverted indices and various sorts of trees, but I would have thought there are more research-y approaches (e.g. low rank tensor decomposition) that if we could figure out how to perform them efficiently would blow the existing methods out of the water. But IDK, I’m not in that industry so maybe I’m overlooking something.

Warm objects actually do weigh more than their counterfactual cold versions haha. The stress energy tensor is the quantity to look at here.

> it's hard to imagine anyone arguing in good faith that you should give those amenities up and move somewhere boring

Oh, that's certainly not why I moved haha. We wanted to be closer to family and that was just one of the unfortunate tradeoffs of that decision. The math and CS topics I've been studying are those that I find intrinsically interestingly (e.g., computability theory), but they are unlikely to benefit my career more than tangentially. I didn't really make that clear above.

With "core motivations" I was referring to what I would like to accomplish over a lifetime, which is more about what actually benefits society in some way (and at least so far, that appears to be orthogonal to my career). Personally, I found that moving somewhere less "interesting" helped me to realign with those objectives. Or maybe that's just post-hoc rationalization.

> one of the most consequential decisions you can make in life is the city you choose to live in

This seems to have had the reverse effect on me. I always wanted to move to the Bay Area growing up because that’s where the tech industry was. When I finally did, I got distracted by all that California had to offer: nature, good food, an endless supply of places to go and interesting things to see. I moved there for tech but promptly lost interest in tech. I picked up a bunch of fun hobbies totally unrelated to my core motivations in life.

Now that I live somewhere boring again, I spend most of my free time learning about new areas of mathematics and computer science.

I’ve also observed the same paradoxical effect with having children. Prior to kids, I had tons of free time that I essentially wasted. But now that free time is scarce, I wake up at 4 AM to study, practice, or create something before the work day starts.

It’s almost like sub-optimal conditions trigger an instinct to fight against those constraints by producing value. If I actually get what I think I want (living somewhere interesting, having plenty of free time, etc.), it’s like I just lose focus and motivation. Go figure.

He mentions it on the second page:

> any Martin-Lof random sequence that computes (i.e. allows computing from it) a consistent completion of PA also computes the Halting Problem H; and by deLeeuw et al. [1965], only a recursive sequence (which H is not) can be computed with a positive probability by randomized algorithms.

It's just the sequence of the solutions to the halting problem, i.e., the characteristic function of the halting set. Levin points out this sequence is not recursive/decidable.

To be fair to [0], Leonid Levin (co-discoverer of NP-completeness) makes a similar but slightly weaker claim in a more formal sense: that no algorithm or even random process can increase mutual algorithmic information between two strings (beyond O(1)), which includes any process that attempts to increase mutual information with the halting sequence (https://cs-web.bu.edu/fac/lnd/dvi/IIjacm.pdf).

Nevertheless, we clearly do have some finite amount of information about this sequence, evident in the axioms of PA or ZFC or any other formal system that proves an infinite number of programs as non-halting (hence why the Busy Beaver project has been able to provably confirm BB(5)). We presume these systems are truly consistent and sound even if that fact is itself unprovable, so then where exactly did the non-halting information in the axioms of these systems “come from”?

Levin stops short of speculating about that, simply leaving it at the fact that what we have so far cannot be extended further by either algorithmic or random means. But if that’s the case, then either AI is capped at these same predictive limits as well (i.e., in the sense of problems AI could solve that humans could not, both given unlimited resources), or there is additional non-halting information embedded in the environment that an AI could “extract” better than a human. (I suppose it’s also possible we haven’t fully exploited the non-halting information we do have, but I think that’s unlikely since we’re not even sure whether BB(6) is ZFC-provable and that’s a rather tiny machine).

I noticed a funny thing a while back after using the “bird’s eye view” capability in my car to help with parallel parking: I couldn’t parallel park without that feature anymore after a few years. It made for an awkward situation every time I visited the Bay Area and rented a car. I realized I had become so dependent on the bird’s eye view that I had lost the ability to function without it.

Luckily in this particular case, being able to parallel park unassisted isn’t all that critical in the overall scheme of things, and as soon as I turned that feature off, my parking skills came back pretty quickly.

But the lesson stuck with me, and when LLMs became capable of generating some degree of functioning code, I resolved not to use them for that purpose. I’m not trying to behave like a stodgy old-timer who increasingly resists new tech out of discomfort or unfamiliarity—it’s because I don’t want to lose that skill myself. I use LLMs for plenty of other things like teaching myself interesting new fields of mathematics or as a sounding board for ideas, but for anything where it would (ostensibly) replace some aspect of my critical thinking, I try to avoid them for those purposes.

I have two lines of thought on this:

1) Chatbots are never going to be perceived as safe or effective as humans by default, primarily due to human fiat. Professionals like counselors (and lawyers, doctors, software engineers, etc.) will always claim that an LLM cannot do their job, namely because acknowledging such threatens their livelihood. Determining whether LLMs genuinely provide therapeutic value to humans would require rigorous, carefully controlled experiments conducted over many years.

2) Chatbots definitely cannot replace human therapists in their current state. That much seems quite obvious to me for various reasons already argued well by others on here. But I had to highlight point #1 as devil's advocate, because adopting the mindset that "humans are inherently better by default" due to some magical or scientifically unjustifiable reason will prevent forward progress. The goal is to eliminate the (quite reasonable) fear people have of eventually losing their job to AI by enacting societal change now rather than denying into perpetuity that chatbots are necessarily inferior, at which point everyone will in fact lose their jobs because we had no plan in place.

So we’ll require RTO for just about everything except paying for flights for in-person interviews, where being in an office might actually significantly matter.

Will never understand the mindset of corporate executives.

I think this is how we get ML models to come up with novel ideas. Diagonalize against all the ideas they’ve already tried and dismissed via self-argument but keep certain consistency constraints. (Obviously much easier said than done.)

Another weird one related to Gödel’s theorems is Löb’s theorem: given a sound formal system F and a sentence s, if F proves that “if s is provable in F, then s,” then F also proves s. That is:

F ⊢ (Prov_F(“s”) → s) → s

Which is strange because you might think that proving “if s is provable, then s” would be possible regardless of whether s is actually provable. But Löb’s theorem shows that such self-referential statements can only be proven when s itself is already provable.

If I had to guess, I would say that of the ones with more than a few states and symbols that do not halt (i.e. reach a static image configuration), modern mathematics (ZFC) probably cannot prove that fact for most of them. The Busy Beaver project managed it for all 5 state, 2 symbol machines on the empty tape, but IIRC they’re uncertain whether BB(6) is ZFC-provable. (Someone from that project correct me if I’m wrong.)

I find that fascinating. Small scale computation (exploring Turing machine behavior, cellular automata, etc.) is mostly considered a curiosity within the hobbyist realm at the moment, but I suspect that will change over time as we develop better and better tools to characterize computation.

There are a lot of parallels between rule-based games like Go and rule-based formal systems like ZFC. It’s interesting that the same techniques used for AlphaGo have not worked nearly as well for finding proofs of famous open problems that we suspect are both 1) decidable within ZFC and 2) have a “reasonable” minimal proof length.

What aspect of efficiently exploring the combinatorial explosion in possibilities of iterated rule-based systems is the human brain still currently doing much better than machines?

> find out what's bothering them, usually something emotional, and you validate it

This is a common refrain of counselors and the field of psychology in general, and yet I can't help but think there's some selection bias at play with regard to the type of personality that is likely to recommend this approach as advice and how well the advice actually works.

Personally speaking, I've never cared whether someone "validates" my emotions (and I often view such attempts as a bit patronizing or insincere). There's a problem to be solved, so let's attempt to solve it or at least compromise in good faith. The resolution to the problem is the most likely way to elicit positive emotions from me anyway.

(I do understand however that some people prefer this validation, and if that's what they want, then sure, I'll attempt to do that.)

> “When the request came to us, I was almost jumping up and down,” says Dr. Irfan Essa, a principal research scientist at Google DeepMind and director of its Atlanta lab.

Wait, what? When did Google DeepMind open an Atlanta office? That seems like a news story in and of itself... maybe I’ve been under a rock the last few years.