Xcelerate

So fly the person out for an in-person interview back like we did in the ancient year of 2019? This seems like a total non-problem to me.

> I thought that it might be a rare chance to invoke the NFL theorem appropriately, but I guess I was wrong

Haha, I wouldn’t feel bad. It’s one of the most misunderstood theorems, and I don’t think I’ve ever seen it invoked correctly on a message board.

> it was hard for a professional working there to describe to their kids what exactly they do all day

I work remotely, and my four year old daughter asked me this morning “How does you being upstairs all day give us food?” At dinner time she always asks me “What did you do at work today?”

It’s a very odd experience trying to describe (justify?) the purpose of Zoom meetings and typing on a computer all day to a little person, and the more I attempted to come up with a coherent and reasonable explanation, the less defensible it sounded to myself as I spoke out loud. Tech is quite a strange industry to be in.

Haha, I had the same experience going from scientific work in grad school to big tech. The phrase “a solution in search of a problem” comes to mind. The additional complexity does create new problems however, which is fine for devops, because now we have a recursive system of ensuring job security.

It blows my mind what is involved in creating a simple web app nowadays compared to when I was a kid in the mid-2000s. Do kids even do that nowadays? I’m not sure I’d even want to get started with all the complexity involved.

> Each lemma in Kingma and Ba's ADAM optimization paper is wrong

Wrong in the strict formal sense or do you mean even wrong in “spirit”?

Physicists are well-known for using “physicist math” that isn’t formally correct but can easily be made as such in a rigorous sense with the help of a mathematician. Are you saying the papers of the AI community aren’t even correct “in spirit”?

> Some years ago, Sanborn began charging $50 to review solutions, providing a speed bump to filter out wild guesses and nut cases

Oh man, oh man, this just gave me a great startup idea. What is the total addressable market of nutcases willing to pay $50 or more to have someone check whether they have cracked some difficult code? Perhaps even with a giant prize attached for cracking it?

> But the inferences of the resulting neural nets is not an algorithm

It is a self-delimiting program. It is an algorithm in the most basic sense of the definition of “partial recursive function” (total in this case) and thus all known results of computability theory and algorithmic information theory apply.

> Formal system is a collection of defined operations

Not at all.

> I don’t think you have to look at humans very hard to see that humans don’t implement any kind of formal system and are not equivalent to Turing machines.

We have zero evidence of this one way or another.

—

I’m looking for loopholes around Gödel’s theorems just as much as everyone else is, but this isn’t it.

> This is patently false.

Ok, I stand corrected.

Suppose an independent researcher with a background in linguistics solves P vs NP. Unlikely but not impossible. Who on earth is going to take a look at their paper? No one credible, that’s for sure.

So even if someone has the funding and the will for independent research, the problem remains of confirming the validity of their research. This is a research problem in its own right. Ideally we have a system of peer review to validate research, but in practice we use a weak form of argument by authority as a loose proxy for reproducibility. This works better for some fields than others. I know I immediately go Scott Aaronson’s blog to determine whether some new “quantum breakthrough” is actually plausible. It’s a decent proxy in this field for correctness. But psychology? Much more difficult to find a good proxy.

Luckily I think mathematics is already moving in a direction that will eliminate the validation problem. Think you’ve solved the Collatz conjecture? Submit your Lean proof to an automated proof checking system hosted on a university website and if it validates, someone famous is going to take a look at your proof even if you never finished high school. We’re not at that point yet, but it’s inching closer. The group that proved the value of BB(5) received a lot of serious consideration of their work despite their unconventional backgrounds due to having a formally validated proof on hand. Without that proof? Hard to say whether the claim would have been reviewed.

> Most simply, it [electron] just exists as a particular distribution of an electrostatic field in space.

Best simple description of an electron I think I’ve heard yet. I wish we would drop all the dumb analogies. From a kid’s perspective (at least what I can recall from high school), these macroscopic analogies mislead you into thinking the laws of physics work differently than what humanity’s best models of physics actually predict.

For instance, I never liked the sense of “arbitrariness” I felt while learning about the periodic table in K-12 school. The diagonal rule. Hund’s rule. The exception to Hund’s rule. And so on. Don’t even get me started on organic chemistry. But if someone had told me “Forget about billiard balls and wave/particle duality. Our best models consists of solutions to simple and beautiful equations that are extremely difficult to solve”, then that would have made a lot more sense to me.

The author of the article describes the truth as “weird math”. I don’t think that’s necessarily the case. Unitarity is aesthetic—it just “feels right”. The correspondence of atomic orbitals to irreducible representations of symmetry groups is beautiful. Why don’t we teach that to kids? You don’t have to go into the mathematical details of group theory, but just let them know these odd shapes originate from symmetry constraints. Much better than my reaction to seeing an illustration of a d_z^2 orbital in high school. I remember thinking “What the heck is that? This subject makes no sense.”

I want financial independence for the sole reason that I can work on interesting problems like this without any outside nagging or funding issues from anyone else (there might still be some judgment, but I can ignore that).

Personally I think governments should fund more moonshot solo or small team efforts because high risk / high reward pays off when you reduce the variance by spreading it out over so many people. But it looks like we’re going headstrong the other direction in terms of funding in the U.S. right now, so I’m not optimistic.

> for one, your 2%ers will look different from mine.

That’s a kind and equitable thought, but I daresay there’s significant overlap between each person’s 2%ers. Some people are just really pleasant to be around—to almost everyone. Others, not so much.

Oh for sure! Wasn’t critiquing your comment at all. I’ve seen the term a lot lately and it just made me wonder how much the industry is using it as a misleading hype factor. E.g., LLMs are “better” than Turing machines because they are operating at a level “below” Turing machines even though the comparison doesn’t make sense, as symbolic computation isn’t referring to the symbol-manipulating nature of Turing machines in the first place.

I’ve never liked that term “sub-symbolic”. It implies that there is something at a deeper level than what a Turing machine can compute (i.e., via the manipulation of strings of symbols), and as far as we can tell, there’s no evidence for that. It might be true, but even a quantum computer can be simulated on a classical computer. And of course neural networks run on classic computers too.

Yeah, I know that’s not what “symbol” is really referring to here in this context but I just don’t like what the semantics of the word suggests about neural networks — that they are somehow a halting oracle or hypercomputation — which they’re obviously not.

This is exactly what’s going on in many situations. For any proposed study, you can ask the question “Is there a possible outcome of this study that would have a strong emotional effect on someone?” If the answer is “yes”, then I’d say it’s more likely than not that the study’s results are already compromised in some subtle way.

Yeah but now I just switch my perspective from thinking of it as a formal deductive system to thinking of it as an optimization problem.

> It's easy for people (especially the kinds of people who gravitate towards engineering) to get all worked up about the necessary implications of the regulations as-written

I was once trying to figure out taxes owed on some RSUs granted in California that vested in North Carolina (and some other edge case that I can’t remember). Hoh boy. What a rabbit hole. I didn’t think the CPA that I hired to do my taxes handled it correctly, so I started digging into the tax laws and regulations. Couldn’t find anything that covered my specific case. So I started digging into court cases involving disputes over RSU taxes owed in North Carolina and found conflicting outcomes.

I brought what I had found back to the CPA who basically said something along the lines of: there is no absolute “rule” for what to do in this case like you’re looking for. We make a good faith effort to mirror what was done in similar prior situations, write a number down, and then forget about it unless you hear from the IRS.

Did not make me feel very confident about the legal system.

Do you mind sharing which platform?

Now we just need a smart person who is somehow unaware of the halting problem.

The name-calling in public discourse wears on me. Ad-hominems, bad faith arguments. I’ve gotten to where I avoid the news altogether because of this seemingly accelerating trend.

The fact that the human brain can still do better on certain types of problems than SOTA LLMs while using less energy than a nice LED lightbulb continues to bolster my belief that ultimately it all comes down to the right algorithm.

That’s not to say data isn’t necessary, but rather that the algorithm is currently the critical bottleneck of further AI progress, which a $10M startup absolutely has a chance of outcompeting big tech companies on. Heck, I wouldn’t even put it past an individual to discover an algorithm that blows existing approaches out of the water. We just have to hope that whoever achieves this first has a strong sense of morality...

Curiously enough, the Downward Löwenheim-Skolem theorem proves that if any first-order theory has an infinite model, then it also has a countable model, assuming the theory itself is countable.

So even though ZFC talks about uncountable real numbers, there is actually a countable model of ZFC that satisfies the same axioms.

This isn’t an inconsistency, but it really does blur the lines between what we think of as mathematical objects that are “out there” in some sense (like uncomputable real numbers) or whether mathematics is just a game of symbol manipulation that also happens to predict the physical world pretty well.

That’s funny cause I’m going the exact opposite direction and trying to remove the diffuse lighting and replace it with very hard and bright lighting that has a spectrum as similar to sunlight as I can find/afford.

Recessed lighting with parabolic reflectors collimates light conically, which is more similar sunlight than omnidirectional lighting that passes through a diffuser. The sun is basically a point source so far away that the light rays that reach us are almost parallel. To me it feels much “cozier” than soft lighting, which gives everything a bland, washed out look and makes me sleepy during the work day.

I was even thinking about replacing my surface mount LED lighting with recessed cans. But everyone is obviously quite different in their preferences haha. If you want more diffuse lighting, there are filters and lenses they sell that you can slide into the cans.

Yep. I’ve been replacing all the bulbs in my house with Yuji SunWave, and the difference is astonishing. I just put in four of their PAR30 4000K bulbs above my kitchen island, and the first time I turned the lights on at night I gasped at how much it looked like sunlight. (Then again, my wife said she couldn’t tell much of a difference and suggested my reaction was possibly confirmation bias, so YMMV.)

They’re quite expensive compared to normal LED bulbs, but it’s hard to argue against the quality of life improvement, particularly in the winter where I work remotely from a home office all day.

I was actually considering setting up an high brightness array of their full spectrum lighting above my desk. I know the article mentions diffuse lighting is best, but for some odd reason I prefer “spotlight” style. I don’t know why—it just feels cozier to me.

One thing I’ve noticed as I’ve learned more about lighting is that the brighter the light, the better cool color temperatures start to look. For a long time I hated anything above 3000K (too “office-like”) but 4000K actually starts looking pretty good around ~7,000 lumens directly overhead, and I imagine 5000K would look alright above 15,000 lumens or so (perceived brightness is a logarithmic function of luminance). IMO 5000K looks downright ghastly in a home setting for the typical range of 500-800 lumens that most bulbs sell at nowadays.

Why do HN commenters want OpenAI to be considered in violation of copyright here? Ok, so imagine you get your wish. Now all the big tech companies enter into billion dollar contracts with each other along with more traditional companies to get access to training data. So we close off the possibility of open development of AI even further. Every tech company with user-generated content over the last 20 years or so is sitting on a treasure trove now.

I’d prefer we go the other direction where something like archive.org archives all publicly accessible content and the government manages this, keeps it up-to-date, and gives cheap access to all of the data to anyone on request. That’s much more “democratizing” than further locking down training data to big companies.

K(x) is the Kolmogorov complexity of x, i.e., the length of the shortest program that halts and outputs x, typically defined with respect to a universal Turing machine.

I(x : y) = K(x) + K(y) - K(x, y) is the mutual algorithmic information of two strings. It is the algorithmic equivalent to Shannon's mutual information. No algorithm f can increase the mutual algorithmic information between two strings, i.e. ∀f I(x : f(y)) ≤ I(x : y) + O(log(K(f))).

I used "data" to denote any collection of interesting data at all. For example, it could be data obtained from the real world, the observed behavior of Turing machines at very long timescales, or a collection of mathematical proofs. By "ZFC" I just mean the description of any program that enumerates all proofs of ZFC.

The takeaway here is that ZFC is very limited in what it can say about real world data or even what it can say about almost all deterministic computations, including those with very short programs. Levin describes this much better than I could in his famous "Forbidden Information" paper: https://arxiv.org/pdf/cs/0203029.

Levin further argues that extending PA is unlikely... I tend to disagree on that point. How did we get the more powerful theory of ZFC or any of these axioms in the first place then? They are coming from somewhere. But I'm not even going to attempt to debate Levin's case on Hacker News haha

> Holding the field back from what? If the goal of the practitioners of the field is to seek mathematically beauty, then well, that is what they will focus on.

Holding the field back from answering questions about the behavior of simple deterministic systems that arguably have an outsized influence on science, machine learning, and mathematics itself. I don't disagree that "beauty" is certainly subjective, but the mathematics research that gets funded by universities and research labs is only tangentially related to such an aesthetic notion.

> In the vast majority of cases, the difficulty in finding a proof of a statement is not that the statement isn't provable under a given formal system, it's that we simply can't find it

Finding a proof is an inherently algorithmic process. Presumably, the human brain uses heuristics (intuition) that have thus far managed to beat simple algorithmic approaches. But it's hard to believe that's going to last much longer. As an extreme example, simply knowing more values of the Busy Beaver function allows one to find proofs more easily. For example, encode the veracity of the statement corresponding to Fermat's Last Theorem into a program (a k-state Turing machine) that dovetails enumeration over all possible values for x, y, z, and n > 2. This program halts if the statement is satisfied by some set of natural numbers and never halts otherwise. But if we know which k-state Turing machine corresponds to BB(k), then we just run the two programs in parallel and if the Fermat program hasn't halted by the time the program for BB(k) has, then the conjecture is true (necessarily false otherwise). Scott Aaronson has written some articles and blog posts about this.

Now the argument I'm making doesn't necessarily depend on trying to determine more values of the uncomputable busy beaver function. You don't have to know the fastest growing computable sequence in order to derive some benefit from greater knowledge of the halting sequence. If we presume that an interesting proof exists within ZFC, then more axioms (that constitute a more powerful system) can lead to much shorter proofs. This is a result obtained from the work of Gödel, Feferman, Jean-Yves Girard, et al. So while you're right that a conjecture we are interested in might have a proof that "exists" within ZFC, whether the minimal such proof can be written down in a human lifespan is a different question. Considering there are many famous conjectures that have been open for centuries now, perhaps the next step isn't having more people stare harder at the problem but rather enriching our foundational formal systems with additional axioms.

I remember when I was looking for new cookware a while ago, there were rumors that Kitchenaid was selling rebranded Demeyere pots and pans. It sure looked like the exact same cookware in the photos. But Zwilling is known to disguise the same pan in 30 different ways, and for anyone willing to trade the "Demeyere" label for a "Kitchenaid" label, they were getting a steal of a deal.

Exactly. I’ve never understood this criticism. A good CEO (in terms of the business) is able to make significant, groundbreaking decisions but is also able to reverse course quickly if those decisions aren’t working out (anyone remember the Facebook phone)?

Unless the CEO is psychic, they’re necessarily going to make a lot of bad or wrong decisions. The key is being able to recover quickly and move on to the next thing. A bad CEO makes no big decisions for fear of being wrong.

When FB bought Instagram for $1B, there were a lot of talk show hosts riffing on Zuckerberg for making one of the stupidest business decisions of all time. A lot of executives who got to their position by corporate ladder climbing have personalities that would be terrified of that sort of widespread criticism. They would never make the kinds of decisions that might possibly put them in the unenviable position of being made fun of on national television.

> is just a DFA

Oh is that all? If resource bounded Kolmogorov complexity is that simple, we should have solved P vs NP by now!

I debated adding a bunch of disclaimers to that parenthetical about when the infinite tape starts to matter, but thought, nah, surely that won’t be the contention of the larger discussion point here haha