roystgnr
13d ago
another independent group has now also reached the solution.
This isn't the solution, though, is it? The only difference between incompressible Euler and incompressible Navier-Stokes is that the former has no diffusive term and the latter does, so I'm certainly not going to suggest Tao was wrong that "There does not seem to be anything in principle preventing the methods from extending all the way to Navier-Stokes", but that diffusive term is pretty important in this specific case if they weren't able to extend their results to Navier-Stokes immediately ... and it's pretty important in this context in general. These are conservative equations where free energy in the system is bounded, so any blowup has to be a localized singularity that blows up larger and larger in tinier and tinier spaces. But, the tinier you get in space, the larger the derivatives with respect to space get, and the harder a diffusive term (which roughly speaking adds a force counteracting large second derivatives) fights against your developing singularity.
If you'd asked me to guess last month, I would have said that I'd expected blowups were possible in the Euler equations and not in the Navier-Stokes equations. In hindsight that would have been ignorance on my part, and probably embarrassing ignorance based on Tao's attitude above, but I still think Navier-Stokes was legitimately a harder problem to solve in this way than Euler was.
LLM solutions are barely readable
Depends on the problem. The Jacobian conjecture counterexample was something a good engineering Bachelors' could understand, and even its derivation seemed like math-grad-student level, at least for students focusing on differential geometry. Very nice.
Some of the other recent big results are so unreadable that I don't even tell anyone about them until I see people are confident in the formal verification. Erdös talked about proofs being "straight from The Book" of God's best proofs of every mathematical theorem, and claimed "You don't have to believe in God, but you should believe in The Book". Humans have also come up with some devilishly-convoluted proofs over the years too, but we at least have the good taste to hate it when that happens.
it still makes sense for academics to do themselves, or at least break the model's solution into something comprehensible by humans, and receive credit for that.
I strongly agree, if by "still" you mean "in Fall 2026". Beyond that? In early 2024 I couldn't get a frontier model to integrate a reaction-convection-diffusion equation by parts and give me a weak form without making a sign error, or get it to correct its sign error without making a different error instead. In mid-2026 they're coming up with proofs "straight from The Necronomicon", but they're proofs for problems that geniuses have failed to solve for decades. At this rate I'd be very surprised if humans are better than late-2028 LLMs at finding simpler proofs or at making the proofs we do have as easy to understand as possible.
roystgnr
13d ago
The progression details never got me to "starting to dislike it" territory, but I do agree that they were the parts of the story I least enjoyed. They felt like they were killing the pacing and my interest.
I can't call them "the worst" or even "my least favorite" parts of the story, though, because when my son read it he ate most of that stuff up, and "repetition is the mother of learning" is exactly the mantra that smart lazy people need drilled into us.
roystgnr
14d ago
That's the cameraman Sharmake Omar (I'm 99% sure - ages on the stories are off by a couple years, and those are apparently popular Somali names, but photo/video looks like a match), not the father Shire Jimale, but other than that I guess "nonce" was probably going easy on the guy.
Thanks for the links; I don't recall seeing that before.
roystgnr
14d ago
5, 3, and 0, not 8.
Did someone here call one of them a nonce, or did you just not understand the reason behind my question?
roystgnr
14d ago
He's got me blocked, so he may have missed my question and the answer recently. I'd worry that I must have done something wrong, but after reading that swath of ignorance-based insults I'm forced to suspect I must have done something right.
roystgnr
17d ago
E.g. the best AIs can only barely play Pokemon games that are meant for toddlers, finishing them in 10x-100x the usual playtime that a human would require.
Are there new benchmarks on this? Best I can find in a quick search is a year old (i.e. 7 dog years, 20 LLM years).
roystgnr
18d ago
viruses and other bacteria inhabit a sort of unstable triangle between lethality, transmissibility, and virality
Germs don't inhabit much possibility-space at all, for the same reason that evolved life forms in general don't: any living thing must be a chain of neutral-to-positive mutations away from a prior already-viable population of living things. You can eventually get sharp claws and powerful wings via a long chain of gradual changes to keratin scales and tetrapod forelimbs, but natural falconry has nothing modern militaries desire or fear, because with intelligent design unconstrained by intermediate-form viability we can just go straight to bullets and missiles and jet engines. Maybe no leaps like that are possible at the nanoscale and microscale? I'm not looking forward to finding out.
roystgnr
18d ago
"our generation"
I coached my first after-school MathCounts session of the year today. One of the kids grabbed a sparkling water from my bag of juices and sodas. The other kids ragged on him: "What are you, thirty-five?", because of course that's like the Pinnacle Of Old to them. I'm about half a generation past that now...
with grey hair
This is my only reprieve; my hair may have thinned to the point where I have to buy spray-type sunscreen or get sunburned through it, but there's so little grey that whatever's there is still managing to hide itself among the dirty-blonde.
roystgnr
19d ago
A valid proof in the mathematical sense is simply one where every single step is justified by either an axiom or an already-proven theorem. You see some of these in a good Algebra 1 class where just going from "z=2(x+y)+x" to "z=3x+2y" uses left- and right-distributivity once each, associativity twice, commutativity once, and identity once. Then if you're lucky you never see them again, at least until you're using a formal proof verifier that actually wants a complete proof, yes, even if it's a hundred times longer. What's in the literature instead are "proofs" where we skip five or fifty steps at a time because we know our audience will be able to fill in the obvious bits inside those gaps between the big checkpoints, even though the definition of "obvious" depends on the audience and is famously a little slippery. So don't feel bad. Even when your audience is a professor, "obvious" still isn't a well-defined adjective and everyone is still stuck trying to intuit it. At least with theses and papers your advisors and reviewers will come back and say "step 23 wasn't clear enough; fix it". With homework or tests requiring proofs, professors' only options are to let it slide or to mark you down if you skipped a step they don't think was obvious.
roystgnr
19d ago
Al Qaeda was so angry at ISIS because they were worse than wrong, they were early.
It'd be funny if Bin Laden actually had read the first Foundation book, and only the first. "I was becoming a military leader who was going to restore the full glory of the Empire Caliphate, but structural-demographic forces caused our own people to undermine themselves! How could we possibly have ever expected something like to happen?! Hush, Marwan; why are you babbling about 'Foundation and Empire'? We don't have time to read now!"
the two greatest titans of early SciFi
Clifford Simak and Murray Leinster?
Only half-joking here - Asimov and Heinlein were the two greatest titans of Golden Age SF, but Asimov at least was very cognizant of and pushed for more long-term recognition of the "Silver Age"/"pulp era" greats preceding them. And Asimov was an utter egotist (in fact, it looks like he backdated a previously-unsalable short story of his own to shoehorn it into that anthology?) so praise from him in his own fields was very high praise.
obviously modeled himself after the main character.
With a few significant divergences. But other than that, Mrs. Tate, how did you like the book?
roystgnr
19d ago
If the story was written from Hermione's perspective, it would be much more interesting.
I'm sorry to join the "reading QCs a month later" pile-on, but I have to ask: are you sure this is true?
I've always thought of it as a bit of genius for Rowling to make Hermione a side character. From a Watsonian perspective Hermione is halfway to being a Mary Sue, but that turns out to be fine, because she doesn't fit the most important part of the Doylist definition of a Mary Sue: she's not Our Main Character. We don't live in her head, we spend a bunch of time away from her, and we don't even meet her until several chapters into the first book, so we don't ever begin to relate to her as a Wish Fulfillment stand-in. She can face a threat capable of incapacitating her for half a book without readers missing the climax. She can be a Double Witch with extra-secret time-turner powers or be the focus of a love triangle with a celebrity athlete, without those things feeling like just a Twilight-style annoying paean to how great Our Protagonist is, because we see those things from the outside. She doesn't need to break characterization and seize the Idiot Ball to get into interesting conflicts, because we get emotionally invested enough into Harry that we don't get too annoyed when he's idiot enough for the both of them. (which he kind of has to be; since he fits a ton of other Mary Sue traits, he'd get pretty annoying too if he wasn't regularly failing and getting smacked around)
roystgnr
20d ago
The intuitions required for formal proof verification are "it's worth rewriting this proof in another language that's an order of magnitude more verbose just so you can get a computer to tell you what you're sure you already know" and "the verifier doesn't have any soundness bugs that will invalidate any of its verifications" Historically the latter has sometimes been untrue and the former has usually been untrue. LLMs are fixing the first problem, which is exposing and leading to fixes for the second problem, but that's all a relatively new development. It's going to take a while to go back through all the mathematical literature and see how much of it might have problems due to predating the coming era of formal verification.
Consider the recent construction of a complex structure on the six-sphere. The simplest English explanation I've seen is under a thousand lines of (admittedly difficult!) writing and mathematical notation. The Lean formalization is a quarter-million lines of code. It's ... probably correct, people seem to think? But if it is correct, the construction would (reportedly; this is outside my field and way beyond me) contradict a 2020 paper (which itself was a correction to a 1998 paper), so we're almost certainly either producing new broken proofs or revealing old invalid proofs here.
roystgnr
20d ago
I've not yet made it through the whole story, which logically does undermine my criticisms of it ... except perhaps for this specific criticism ...
roystgnr
21d ago
I'd recommend Project Lawful by Eliezer Yudkowsky (LessWrong) and Kelsey Piper (The Unit of Caring)
To someone who just specifically listed "get rid of sixty percent of the text" as something that would improve most web fiction?
roystgnr
21d ago
I haven't read author commentary, so you could be right. My read is that
IIRC the other big perspectives that might engender disagreement (or stronger disagreement, when there's disagreement presented in-story):
roystgnr
21d ago
There's basically three types of "great men" in the Foundation books. There's the ones who can learn psychohistory, and they really do fit the "great men of history" historian-speak definition, figuring out how to steer history using what they learn. There's the ones who can't learn psychohistory (either because they're just not among the galaxy's geniuses and/or because the psychohistorians deliberately kept it from them to keep their steering from being upset), and a society full of the latter is basically running on History From Below rules with no Great Men in the historian-speak sense, despite having great men in the colloquial sense. And there's [redacted due to spoilers], who don't appear for a while, for Watsonian "that was really improbable until whole centuries had elapsed" and Doylist "the arc plot really needed a twist by the time whole books had elapsed" reasons.
After Hari Seldon, the "great men" in the Foundation stories are basically the people whose skill is "be clever enough to realize that there's only one solution to the crisis besetting them, then use it" at best, and it's not even clear to what extent that's necessary because there are other cases where the heroes fail to see the right solution but it essentially enacts itself under their noses.
roystgnr
21d ago
very clearly elucidating a perspective I strongly disagree with
I'd love to find out what you're talking about here. The obvious candidate that jumps to mind is
roystgnr
21d ago
Wales actually has a handful of great short stories. IMHO they're better on average than his long fiction!
Also, although I loved Worth the Candle, it's long and some of its twists and turns are controversial. IMHO every revelation was utterly sensible in hindsight and made a good story even better, but de gustibus non disputandum, and I recognize that if I didn't like a major twist after I'd read 200-odd chapters to get to it I'd be massively disappointed.
You might try his The Metropolitan Man. Fan fiction, but a great combination of clever reconstructions and deconstructions that lead to unique differences from the canon. 80k words, so more "short-length web novel" than medium-length, though.
roystgnr
22d ago
I was taught "records" at some point, but on the other hand it's been 40 years since my first trip to a "Museum of Natural History" where it was considered unremarkable that "Natural" basically meant "Pre-".
roystgnr
22d ago
just because it wasn't practical for some rando writing a weird one-off novel in the universe to talk to the chief
This seems like an easily mostly-solved problem: if the suits are confidently unanimous you don't bug the chief; if not, you send a quick email, archive the response, and summarize it in the Show Bible.
Not a perfect solution, since the suits might be unanimously idiots or might have not seen some foreshadowing or planning that part of "established" canon was a lie, or the chief might still change his mind later and not care that a random novel gets invalidated by it, but still better than adjudicating canon by majority suit vote.
roystgnr
22d ago
Harry Potter as an example is kind of strange. Harry's parents being dead is intro backstory. Mid-book 1 you find out that Wizard Hitler murdered them. Book 1 climax, you learn WH is coming back. Clearly there's some deadly shit about to go down.
Yet it takes until Book 4 before we get a major character death, and Book 6 before we get one that Harry and the readers really care about! The Watsonian explanation (Dr., not Emma) appears to be that Wizard Hitler is just even more outnumbered and incompetent (excepting the wizardry) than Regular Hitler was, and needs to lay low a lot, but the Doylist explanation is clearly that Rowling knew she was writing for kids and needed to pull her punches a bit.
For it's validity, yeah. There's something disquieting about getting proofs "straight from The Necronomicon" rather than "straight from The Book", though.
The full statement of the problem had better be much much less than a quarter million lines; one of the unavoidable ways to screw up a formal proof and still have it pass verification is to make a mistake in the problem statement and so end up proving something other than what you thought you proved. Nobody's going to check a quarter-million-line problem statement for misstatements.
(But I don't think that was an issue here - looks like everything they needed to define the problem was already in Mathlib)
The proof, though? Follow that github link, download and
wc -l Solution.lean: 248818 lines.More options
Context Copy link