Soteriologian
21d ago
Part of the misunderstanding is the word "proof" has different flavour in classical mathematics vs theorem prover math, which is why the word is rarely used in this world except when appealing to legacy mathematicians. The native vocabulary is "3 is a value of type Nat" or "Refl is a value of type 0 + 0 = 0". A legacy mathematician would use the word "proof" only to describe the latter, and think it odd to use the word for the former. But internal to the formal logical framework, these are same notion, and so they should have the same word.
Soteriologian
21d ago
I wouldn't read too much into this. Has anyone ever seen him use a theorem prover other than Lean? If anything, he's a lot more explicit about using the Lean "brand" than the OpenAI brand. Yet obviously he's not a sponsored shill for Big Lean (because there is no Big Lean).
What's clear is his organisation is pursuing private funding since the government axed his grants. I think it's likely OpenAI is among them given his appearance on their Twitter promo. Whether there's any exclusivity contract, who knows, I don't have a confident assessment.
Soteriologian
21d ago
Are they selling these things as proof of applicability to software verification?
I mean, that was certainly my impression. Maybe I've self-selected into circles where that's the sort of thing people naturally care about, and incorrectly assumed this is how everyone is thinking.
Sure, if all you care about is Erdos problems, I guess much of what I'm saying is moot. But this whole "Mythos is finding all these vulnerabilities, the whole meta has shifted!" narrative sure leads me to the next part of the story of "Ok, so how do we actually build stuff correctly in the presence of tools like Mythos?" Because the mythos story, like the classical theorem prover story, is also basically invulnerable to the primary problem of LLMs, hallucination. If the model hallucinates a vulnerability that doesn't work, just throw it away and try again! (Or, in the case of low-human capital, spam the issue tracker with bogus vulnerability reports. But I digress).
Soteriologian
21d ago
I don’t think we’re referring to the same constructivism. I’m referring to this: https://en.wikipedia.org/wiki/Constructivism_(philosophy_of_mathematics)
Well, in the classical mathematical sense, crypto doesn’t work at all: just factor the composite number. The entire premise relies on the relatively ill-specified (by mathematical standards) notion of relative computational cost disparity.
What is the sense in which you claim proofs to be "interchangeable" in classical systems
What I mean is when I sit down to write something in a theorem prover, I speak in terms of Peano nats and inductive lists. When I write software anyone would ever want to actually use, I use machine ints and arrays. There is definitely a sense in which I’m doing the same thing in both cases, but nailing this down precisely is… well, non-trivial. (aka, a royal pain in the ass). Like, the discrepancy here is show-stoppingly problematic.
EDIT: basically, the computation is relevant, and more specifically the speed of computation is also relevant, both in terms of practical usability and outright security in the case of crypto. In the classical world, there is no notion of computational relevance at all -- in fact, you outright end up with these counterintuitive weirdo theorems like Zorn's Lemma. The counterintuitiveness depends entirely on this conspicuous lack of computational awareness in the model: as soon as you put that ingredient back in, you're in the construcivist world, and silly results like Zorn's Lemma don't hold anymore unless you postulate them. My contention is the class of problems for which one can say "I don't care about which proof, just that one exists" is relatively narrow and of little practical relevance (in the sense that one can get an incomputable proof, which is, in a fundamental technical sense, useless), while the class of problems about which one does care which proof, in the Curry-Howard sense, is large and of enormous practical consequence. I want to argue that enthusiasm over the former should not translate to enthusiasm about the latter.
Soteriologian
21d ago
I think crypto is a good analogy. There is actual tech there, and many do indeed believe in it (me being among them). But the hype and noise was wildly disproportionate to what was realistic and done.
At this point, if you put your bet on anything other than "Slightly improved Bitcoin with privacy that was obviously intended originally but not known how to do at the time," you’re probably down 70+%, if not entirely liquidated. Entire narratives about "business on the blockchain!" were complete nonsense.
Fun fact: Sam Altman himself launched a crypto coin back in the heyday. It's down 96%.
Soteriologian
21d ago
as in you hope non-technical readers will look at it and walk away with an understanding like "what Terry produces with his AI is not a real proof"?
Come on, that is not an honest reading of what I said.
In constructive systems, one proof—in the Curry-Howard sense—is not interchangeable with another. For example, you can sort in O(n^2) (or worse), which would be a perfectly valid thing to do in classical mathematics, but a big oopsie in formally-verified software. This is doubly-so in cases like cryptography, where almost none of the "incorrectness" of compromised crypto is incorrect at all in the classical mathematical sense. Further, as someone who has a fair bit of experience playing around with these systems in the past, theorem provers often induce you to write code in a way that is easy to make formal statements about, rather than in a way that actually runs well enough that anyone would want to use it.
My point is the software verification story—which is surely of high importance to businesses—is far more nuanced than "throw the clanker at Lean and let it churn". I think the bucket of cold water I’m tossing is completely justified (even as someone who does indeed buy the baseline premise—that LLMs will be a big boon to working with theorem progress).
Soteriologian
21d ago
The primary smell test is if a person promoting something is only using one brand.
Typically, yes, but we're unironically talking 160+ IQ here. He certainly has negotiating power and some sense of dignity and taste. Anyway, yes, I freely concede my searches specifically for "OpenAI gives TT a bunch of money" were in vain. But they did turn up his new foundation, which comes remarkably close to confirming my original conspiracy theory right on the tin. He’s clearly salty about losing that government money (and rightly so), and is pivoting to asking for private sources.
Soteriologian
21d ago
I made a comment recently speculating that Terence Tao may be a paid promoter of AI. After some off-site discussion elsewhere, our resident shaman on whom the mods cast a long-duration silence posted my comment as a circus exhibit on Twitter to demonstrate a dangerous form of psychosis. Fortunately, OpenAI deemed this a worthy time to intervene and publish an ad featuring Terence Tao, who has taken time out of his busy schedule to assist this struggling non-profit with their promotional.
I want to dissect what I think is really going on.
For starters, every time I sit down to watch WoW on YouTube, I'm greeted with my favourite streamer telling me about the super fun game Raid Shadow Legends, which I should definitely download and play because it's super fun. Is the OpenAI-Terence Tao relationship like this? Not really. Terence Tao does appear to actually spend some time playing around with LLMs. Further, he's not exactly saying a bunch of empty marketing blather, either. In fact, probably to the annoyance of some readers here, I want to take a couple paragraphs for a technical aside, because there is actually subtlety here. I'll bound this in horizontal bars so non-technical readers can skip it:
The main talking point is that automated theorem proving is a perfect fit for LLMs precisely because it's not vulnerable to their main catastrophic failure mode: hallucination. The model can hallucinate whatever it wants, but the text still goes into the theorem prover, and if it's bullshit, well, the prover just rejects it and you query the LLM again. Do this in a loop, burn whatever unholy amount of compute you want, and if the loop stops, you've got yourself a proof! (Well, or a bug in the theorem prover. Or a "You've run out of tokens on your budget" error message. But I digress). This story is largely true. There's a giant asterisk of "Uh, so how much compute we talkin' about?", and the answer is "As much as you need or can afford, whichever comes first!" Which is, of course, the business model.
I will point out one additional technical nit-pick that annoys me because Terence Tao is working in Lean 4, which is a dependently-typed theorem prover. In classical mathematics, one is concerned solely with whether a theorem is true or false, and the structure of the proof is basically irrelevant as long as it's valid. Lean 4 is not based on this model. Rather, it's based on a more computationally-motivated model of mathematics pioneered by Brouwer in the early 1900s called "constructivism." In this world, the question isn't the boolean notion of "Is this theorem true or false?" but rather the related but distinct notion of "Which proof do you have?" To ground this in practical terms, consider the following example: I can prove that True|False and Yes|No are isomorphic, but I can do so in multiple ways: I can map True to Yes and False to No, or I can map True to No and False to Yes (and then show that there are respective inverses which preserve identity, obviously). It is in this sense that one can meaningfully say "Which proof of isomorphism?" when I say I have a proof of isomorphism. Perhaps this all sounds like technobabble, but to connect it to the preceding paragraph: you can immediately see how this does reveal some cracks into the narrative being sold there. It does actually matter which proof is produced, not merely in a social sense of "can any human understand this wall of text the LLM spit out", but in a technical, computationally-relevant sense. For pure mathematics, this distinction is often not considered important -- in fact, many classical mathematicians aren't even aware of the difference, and will be confused if you try to explain it to them and think this is all a bit silly. However, it's not a silly or minor distinction for the following reason: one of the motivations of this computational model for "theorem provers" (it's really a programming language + compiler, rebranded for mathematicians) like Lean is so that formal methods can be applied not just to classical mathematics, but to software in general. And as soon as you enter software formalisation, this distinction is no mere intellectual curiosity, but of paramount relevance. The classical-style logic in the preceding paragraph does not apply to constructivist logic used for software formalisation! I'm sure this distinction is not lost on Terence Tao. But that doesn't concern OpenAI. OpenAI is more concerned with whether the distinction will be lost on the MBAs listening to Terence Tao, and the answer is "absolutely."
Ok, no more technical details like that, I promise. Back to the social level:
So, I mentioned Raid Shadow Legends is a poor metaphor for the OpenAI-Tao relationship. Let me propose some better ones: Michael Phelps and Wheaties (with the added benefit that Terence Tao never smokes weed. See, this is why mathematicians are better than athletes), or better yet, attending Harvard University. This may seem like a strange juxtaposition, but I've done so intentionally, because the marketing is obvious in one but subtle in the other, but it's actually the same trick: the goal is to misattribute performance. With Wheaties, the goal is to sell the notion that Michael Phelps is a great swimmer because he has a healthy diet of stuff like Wheaties, and if you eat Wheaties, maybe you'll perform well, too! Of course, in reality, he was eating sugar-coated french toast and chocolate chip pancakes because he needed 10k Calories/day just to break even on energy, and the reason he's such an awesome swimmer is in large part genetics. Wheaties, or anything similar to it, has virtually no relevance to Michael Phelps at all. But what about Harvard?
Well, Harvard sells the image so well that most people outside this forum outright believe the illusion. The illusion is, of course, that attending Harvard makes you smart and likely to succeed, rather than Harvard accepting only people who were smart and likely to succeed in the first place and thus redirecting credit for these future achievements to Harvard. Mark Zuckerberg may see Harvard as a pointless waste of time, but the world sees Harvard as "The university that made Mark Zuckerberg happen!"
I like the Harvard analogy because this is surely the intent with Terence Tao. There's a high chance sooner or later Terence Tao will prove something cool "using" ChatGPT, and if he does, it would be really awesome if we could make it sound like the secret ingredient in the ChatGPT-Terence Tao alliance was ChatGPT, when obviously the actual secret ingredient is Terence Tao. The analogy I always use for this is stone soup, a European folktale where starving travelers dupe gullible townsfolk into helping them make soup from stones by requesting "extra" ingredients bit by bit until they've just made actual soup, thus astonishing the gullible townsfolk.
There are a lot of other things I could say on this, especially on the technical side, as there are a lot of clever tricks you can pull to make it look like a model is doing more than it really is, but I'll stop for now and conclude with this:
Just be cognizant that OpenAI, and all the other LLM vendors, do marketing. They have an enormous budget that dwarfs anything you have ever seen before. Remember the reality distortion field of Black Lives Matter? Or trans people? Imagine that, but like... two orders of magnitude larger. That is the level of persuasive pressure we're dealing with here.
Just take it all with a grain of salt.
Soteriologian
22d ago
A truly ostentatious change would be to make the $250 bill orange instead of green.
Soteriologian
22d ago
"First principles" here means the balance between (an)aerobic respiration and photosynthesis. That's like 8 orders of magnitude more "first principles" than ediacaran biota.
People can say "the honeybee can't fly by appeal to first principles", but that's just an empty syntactic reference to first principles because it sounds cool, not an actual argument from first principles.
I wouldn't say that. Even if you do grad school, you're still out by 25, unless you do a doctoral degree of some sort, which is a pretty tiny percentage of the population. There's plenty of time to have a couple kids starting then.
The problem is that 25 isn't the starting point! The issue is you typically went off to another city for university, which made you lose contact with your high school girlfriend(s), then go to yet another city to actually settle down after that, so you lose contact with all your university girlfriend(s), and so by the time you're 25 you likely don't even have any serious marriage prospects because you and everyone around you keeps relocating to different places. This is a ridiculous social model.
If everyone would just stay put for a while, I think the issue would resolve itself. For example, the Mormons don't have much issue settling down and getting married, and they're not exactly operating under an 18th century apprenticeship mentality. But they do all go to the same university (BYU), so while they are relocating in a technical sense, they're all relocating to the same place, so it doesn't really count in the same way it does for normal kids, where everyone scatters to the four winds after high school graduation and never sees each other again. That, and BYU is a university that actively encourages them to marry, rather than presenting marriage as some icky distraction from study.
Soteriologian
23d ago
I thought school was a monumental waste of time and hated nearly every minute of it. Now that I'm an adult, I'm even more miffed at all the people around me who tried to gaslight me into thinking it wasn't. I was absolutely fuckin' right about that.
Compulsory education is a repulsive mockery of genuine scholarship. I hate the people who defile the noble legacy of academia with this metric-chasing midwittery.
Soteriologian
23d ago
Yeah, the most significant change in education IMO is the normification of leaving your hometown for university. Catastrophic social norm by Darwinian standards.
Soteriologian
23d ago
It's always a bit tricky to figure out what happened a long time ago, so I freely concede the error bars are enormous. Still, from first principles and basic biochemistry, the GOE does make a lot of sense -- which is how the hypothesis rose to such prominence in the first place.
Soteriologian
23d ago
Humanity is actually really good at solving these problems. There was a time when all life on earth was nearly driven extinct by drowning in its own excrement (no, it's not a link to the Ganges river in 2026, you can safely click it). We're pretty solid by comparison.
Soteriologian
25d ago
Good post overall, addressed a lot of my interjections as I read through it.
The thing is I think the premise is sort of a category error: "Be honest about why you don't want children" is basically resolved as "because you just don't want to, not some hallucinated moral justification." But "You don't want children because you don't want children" is not exactly an insightful notion: as your post notes, nobody in the past seems to have had this problem. And from first principles, Darwinian dynamics imply normal people do want children, as the ones that don't will mostly be wiped from the board each generation, selecting for those that do. Yes, there's some conflation between wanting sex and wanting children, but it would be silly to contend these are fully independent: we have abortion now, yes, but they had abortion in the past, too, it was just post-birth abortion, so I think the distinction is more one of modern sensibilities than one that would be of Darwinian relevance. Having children is pretty much universally seen as a good thing, if not an outright divine blessing, in human cultures across time and space. Further, even if you cut the abortion rate to 0, we'd still have well below replacement fertility.
So why did people stop wanting children? Many contend they didn't: they stopped having children, yes, but they didn't stop wanting children.
I think there are many reasons, but one reason I think is significant but rarely noted is that the campaigns against teen pregnancy have, thanks to the rise of rationalism, finally been successful. In the past, when Christian norms reigned, sex education was basically a crotchety old woman badgering you to behave yourself because an invisible man in the sky said so, and obviously teenagers don't care what some crotchety old woman says about an invisible man in the sky, so they do what teenagers do, have an oopsie, then a shotgun wedding where we all pretend to not know what's going on, and then you're left with a healthy family. Traditional sex education, in a nominal sense, completely failed to do its job -- though in a Darwinian sense, it very much succeeded! But today, rational autists have analysed the situation and concluded "Oh, if we want to prevent teenagers from getting pregnant, having a crotchety old woman tell them about an invisible man in the sky is obviously an ineffective tactic. What would actually be effective is showing them lots of pics and footage of sexually-transmitted infections!" Well, as it turns out, the rationalists were correct, and the teenagers did indeed finally start behaving as the tradcons say God intended, and now we're facing the judgment of Darwin. The fertile demographics, of course, have largely eschewed this rationalist nonsense, and continue to use the ineffective form of sex education, as God intended.
Soteriologian
26d ago
I think this is a real phenomenon, but Epstein is a terrible example. Epstein was bringing in low-class prostitutes and passing them around to his friends. He was running a prostitution ring, not seeking to find an untarnished dame for his hand in marriage.
Soteriologian
26d ago
Part of the reason narratives conflict is that there really are people who just marry their high school sweetheart and stay happily married for life. In fact, the fertile demographics are primarily composed of such people.
But yeah, if you miss out on that, move away from your hometown, and try to find love in the club or on a dating site, well... yeah, that's a different world. People are more broken there, everything is messier, and there's no community that radiates an aura buff for healthy, long-term relationships. Children become a liability, divorce settlements loom like a sword of Damocles, etc.
the polite fiction that women (and society) want them to be nice above all else
"Niceness" is the wrong word for what most women want in a man. I think it's less of a lie/polite fiction than a viewpoint error. The ideal man is more like a German Shepherd: the dog is friendly and playful among those it knows and trusts, and is hostile and aggressive against those it does not -- especially when they pose any sort of threat to those it knows and trusts. You can leave your toddler alone with the dog without a care in the world that the dog will bite it or attack it. But obviously this in no way implies the dog is incapable of violent aggression: you want vicious aggression when an intruder enters your home! It is the proper discretion of when to be friendly and when to be violent that makes this dog radiate such an aura of safety.
Putting the above three paragraphs together, it's easy to see what's going on: in the high school sweetheart case, there was never any need to treat this person as an outsider because this is someone you've always known since childhood. But a stranger in the city you met in a club? Obviously you cannot treat this person like you would a childhood freind. They are a threat, in some sense, and you're a miscalibrated fool to not treat them as such. They definitely can just have sex with you and ghost you, give you an STD, badger you into giving them money, bring in drama with their ex(es), or goad you into signing a marriage document then waltz off with half your money. It takes a fair amount of work to overcome this trust barrier, and often it's never overcome and no long-term relationship forms.
As for sluts, well... I think this word is also too big. There are prostitutes, people who engage in casual sex, and adulterers, and IMO these are quite different, especially the latter. Historically, I think these were often conflated because of the culture-defining preeminance of pathogenic threat (even if not consciously reified as such), which rendered any non-monogamous sex extremely dangerous. Today, to at least to a decent extent, the pathogen threat can be mitigated: antibiotics and similair treatments are effective for many diseases that would have been showstoppers historically, and if nothing else, we at least have tests so you know whether the person is infected in the first place. I think adulterers now stand out as much worse than the other two, as there's been a breach of trust. Prostitutes, well... the old saying comes to mind: "There are two kinds of men who pay for sex: those who are paying you to come, and those who are paying you to leave." With prostitution, at least, nominally, there's no breach in trust. Arguably, it's just a poor woman's method of searching for a good mate -- a man in the latter category who will hopefully one day decide not to pay her to go away. As for casual sex, I think the dynamics are much the same as for prostitution, it's just for women with enough access to money to find explicit prostitution uncouth (although the social norms for dating, namely "man pays for everything", basically make this tantamount to prostitution, just without calling it that).
Are men attracted to sluts? Eh, men are attracted to women, and sluts are mostly all that's available if you fumbled the high school sweetheart route. I mean where would you even go to encounter a non-sexually-active woman where it would be appropriate to make a sexual advance? The nun archetype exists for a reason: adult women who aren't married or sexually active select themselves into circles where they'll never be approached by a man at all. In The Sound of Music, the Reverend Mother basically boots Maria out of the abbey and into a governess job for this reason: Maria clearly doesn't belong in the abbey; she's supposed to be with children and a good husband. Alas, the role of Reverend Mother seems to have been lost to time.
Soteriologian
28d ago
Nah, this is pretty common. Like if you read Maxwell 1865, it looks nothing like the modern presentation of Maxwell’s equations. It’s not because people are lying, it’s because the underlying idea has been substantially cleaned up from the first person to stumble upon it.
Another example: calculus didn’t even have any rigorous foundation until a century after Newton, when Cauchy finally came up with the modern epsilon-delta thing we teach everyone today.
Modern presentation is only wrong in the sense that it’s biased towards presenting the polished ideas in their final state, while attributing this to the original thinkers, when in reality, there’s usually a big story between "guy who originally thought of this" and "what we’re actually presenting to you in class today."
The Gaussian distribution is another example. The distribution itself was proposed by Gauss, yes, but the justification for why this distribution is indeed the peremptory-correct distribution was done by Laplace (who had proposed several prior attempts at his own normal distribution!) The logic of why the normal distribution is the normal distribution—what we now know as the Central Limit Theorem—is the meat of the story, and yet Laplace’s name is merely a footnote to anyone except math nerds.
Soteriologian
28d ago
Currently reading Descent of Man by Charles Darwin. What's striking to me is how much of a not-Darwinist Darwin is. I mean, he's a naturalist, yes, but check this out:
As the voice was used more and more, the vocal organs would have been strengthened and perfected through the principle of inherited effects of use
That sounds like Lamarckism to me. Bro be out there batting for the other team. And it's not like he wrote this when he was 12, before he had his head screwed on straight. This was toward the end of his life!
The classroom story we were told about the history of evolution, at least in my school, was very misleading. In my school, we were taught Lamarck was basically the Aristotle of evolution, saying a bunch of harebrained nonsense he made up, and Darwin was basically Newton who came along and explained how it akshually worked. But that is not at all how this played out.
Soteriologian
29d ago
The problem with all these demos is that the level of capital involved is well beyond what it would take to simply contract some world-class humans to do their thing and misattribute their work to AI.
Like Terence Tao’s enthusiasm for AI seems, uh, kinda synthetic tbh. I’m like 90% sure he’s contracted to use these fancy models and try to get them to do something cool, then post about his experience, with the tacit understanding that further contract money is dependent on him not saying "Well, that was interesting, but basically a waste of time. Back to doing what I was going to do anyway." If you really want to put on the tinfoil hat, he was placed in a precarious financial situation to help motivate him, which was definitely not coordinated or planned by the people who coordinate and plan everything. If there’s one thing the Trump administration would never do, its leverage state policy to manipulate markets.
I think you've never spent any time with a formal theorem prover lol. You're conflating the definition of
+with the proofRefl : 0 + 0 = 0.Mathematicians can say whatever they want, but the story here is about mechanically-verified formal verification, and this is how formal verification works, whether legacy mathematicians think this pedantically or not.
More options
Context Copy link