Xcelerate

7 ms·

61.
by Xcelerate 1y ago
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
62.
by Xcelerate 1y ago
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", &quo
63.
by Xcelerate 1y ago
Thanks for sharing! I didn’t think about all of the intermediate steps that might be difficult to encode, but that makes sense.
64.
by Xcelerate 1y ago
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
65.
by Xcelerate 1y ago
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.
66.
by Xcelerate 1y ago
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 art
67.
by Xcelerate 1y ago
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 th
68.
by Xcelerate 1y ago
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?
69.
by Xcelerate 1y ago
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 ignori
70.
by Xcelerate 1y ago
> 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 derivabl
71.
by Xcelerate 1y ago
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
72.
by Xcelerate 1y ago
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 consisten
73.
by Xcelerate 1y ago
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 prim
74.
by Xcelerate 1y ago
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.
75.
by Xcelerate 1y ago
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 min
76.
by Xcelerate 1y ago
Warm objects actually do weigh more than their counterfactual cold versions haha. The stress energy tensor is the quantity to look at here.
77.
by Xcelerate 1y ago
> 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 un
78.
by Xcelerate 1y ago
> 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 w
79.
Almost von Neumann, Definitely Gödel: The 2nd Incompleteness Theorem's Story [pdf](sites.units.it)
1 points by Xcelerate 1y ago|0 comments
80.
by Xcelerate 1y ago
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
81.
by Xcelerate 1y ago
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 (b
82.
by Xcelerate 1y ago
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
83.
by Xcelerate 1y ago
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 al
84.
by Xcelerate 1y ago
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.
85.
Equational Theories Project(teorth.github.io)
2 points by Xcelerate 1y ago|0 comments
86.
by Xcelerate 1y ago
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.)
87.
by Xcelerate 1y ago
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 beca
88.
by Xcelerate 1y ago
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 p
89.
by Xcelerate 1y ago
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 tha
90.
by Xcelerate 1y ago
> 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 a

More ›