kevinventullo

(Also, I love this. I hope you’re still hosting it once I have kids)

We talk about the dotcom bubble, in which there were of course growing pains in figuring out what makes a viable internet-based business, but at the end of the day that era did produce multiple trillion-dollar companies.

Then you have the crypto bubble which really seems to be shaping up to be a nothing burger.

As for today, I think LLM’s are already pretty clearly useful, and they seem to be getting more capable with each passing year. In principle, these models are just the core foundations, while a wide variety of applications are in the process of being fleshed out. I think the jury is still out on how disruptive and effective these applications will be, both from a business/PMF perspective, but also in terms of the raw capabilities.

So take something like Harvey AI. They just raised a round at a $5B valuation, despite having an annualized revenue of just $75M as of April. So is that overinflated? Well, the total Legal Services market has a valuation of about $1T, and given how much legal work is incredibly laborious reading, analyzing, and writing text, (things which LLM’s are already pretty good at), it doesn’t seem ridiculous on the face of it that a Legal-focused LLM product couldn’t add 0.5% worth of efficiencies/value.

“We believe that Palestinian rights must be achieved without harm coming to any other group or people”

“My Judaism is not Zionism”

“F** Israel” (without the asterisks)

“Jews Say No To Genocide”

“UC you have blood on your hands”

“Filmmakers for a free Palestine”

“Fund our jobs and education not war and occupation”

“Never again means never again anywhere!”

“Free Palestine” with a drawing of a policeman, gun drawn, facing a soldier on fire; clearly evoking https://en.m.wikipedia.org/wiki/Self-immolation_of_Aaron_Bus...

“Israeli against genocide”

“UCLA funds war”

“Our liberations are tied”

“Life in everything yearns for the death of occupation” (had trouble parsing this one)

“From Palestine to Mexico border walls have got to go”

This one’s cut off but it ends with “…violation of international law not anti-Jewish bigotry”

A sequence of maps of Israeli/Palestinian borders in 1947, 1967, present day. The map legend labels are “Palestinian Land” and “Jewish/Israeli Land”. There is also a text-based “timeline” starting in 1948, focusing mainly on Palestinian deaths and displacements.

I’m saying that the view of formalized languages as a crutch is backwards; they are in fact a challenging constraint.

The most extreme version of my position is that there is no such thing as a rigorous natural language proof, and that humans will view the relative informality of 20th and early 21st century mathematics much like we currently view the informality of pre-18th century mathematics.

This is a wildly uninformed take. Even today there are plenty of basic statements which LLM’s can produce English language proofs of that have not been formalized.

I completely agree that a machine-generated formal proof is not the same thing as an illuminating human-generated plain-language proof (and in fact I suspect without further guidance they will be quite different, see my other stream of thought comment). However, I do think machine-generated formal proofs would be interesting for a few reasons:

1. Sometimes the obvious thing is not true!

2. I think the existence or non-existence of a machine-generated proof of a mathematical claim is interesting in its own right. E.g. what kinds of claims are easy versus hard for machines to prove?

3. In principle, I would hope they could at least give a starting point for a proper illuminating proof. E.g. the process of refinement and clarification, which is present today even for human proofs, could become more important, and could itself be machine-assisted.

That said, letting machines go wild in the depths of the consequences of some axiomatic system like ZFC may reveal a method of proof mathematicians would find to be monstrous. So like, if ZFC is inconsistent, then anything can be proven. But short of that, maybe the machines will find extremely powerful techniques which “almost” prove inconsistency that nevertheless somehow lead to logical proofs of the desired claim. I’m thinking by analogy here about how speedrunning seems to often devolve into exploiting an ACE glitch as early as possible, thus meeting the logical requirements of finishing the game while violating the spirit. Maybe we’d have to figure out what “glitchless ZFC” should mean. Maybe this is what logicians have already been doing heh).

I think I have a minority opinion here, but I’m a bit disappointed they seem to be moving away from formal techniques. I think if you ever want to truly “automate” math or do it at machine scale, e.g. creating proofs that would amount to thousands of pages of writing, there is simply no way forward but to formalize. Otherwise, one cannot get past the bottleneck of needing a human reviewer to understand and validate the proof.

I think the problem is that “objective indicators pointing to the cliff” is pretty handwavy. Could there be a widely agreed-upon function of qubit fidelity, error rate, coherence time, and interconnections that measures, even coarsely, how far we are from the cliff? It seems like the cliff has been ten years away for a very long time, so you might forgive an outsider for believing there has been a lot of motion without progress.