This weekly roundup thread is intended for all culture war posts. 'Culture war' is vaguely defined, but it basically means controversial issues that fall along set tribal lines. Arguments over culture war issues generate a lot of heat and little light, and few deeply entrenched people ever change their minds. This thread is for voicing opinions and analyzing the state of the discussion while trying to optimize for light over heat.
Optimistically, we think that engaging with people you disagree with is worth your time, and so is being nice! Pessimistically, there are many dynamics that can lead discussions on Culture War topics to become unproductive. There's a human tendency to divide along tribal lines, praising your ingroup and vilifying your outgroup - and if you think you find it easy to criticize your ingroup, then it may be that your outgroup is not who you think it is. Extremists with opposing positions can feed off each other, highlighting each other's worst points to justify their own angry rhetoric, which becomes in turn a new example of bad behavior for the other side to highlight.
We would like to avoid these negative dynamics. Accordingly, we ask that you do not use this thread for waging the Culture War. Examples of waging the Culture War:
-
Shaming.
-
Attempting to 'build consensus' or enforce ideological conformity.
-
Making sweeping generalizations to vilify a group you dislike.
-
Recruiting for a cause.
-
Posting links that could be summarized as 'Boo outgroup!' Basically, if your content is 'Can you believe what Those People did this week?' then you should either refrain from posting, or do some very patient work to contextualize and/or steel-man the relevant viewpoint.
In general, you should argue to understand, not to win. This thread is not territory to be claimed by one group or another; indeed, the aim is to have many different viewpoints represented here. Thus, we also ask that you follow some guidelines:
-
Speak plainly. Avoid sarcasm and mockery. When disagreeing with someone, state your objections explicitly.
-
Be as precise and charitable as you can. Don't paraphrase unflatteringly.
-
Don't imply that someone said something they did not say, even if you think it follows from what they said.
-
Write like everyone is reading and you want them to be included in the discussion.
On an ad hoc basis, the mods will try to compile a list of the best posts/comments from the previous week, posted in Quality Contribution threads and archived at /r/TheThread. You may nominate a comment for this list by clicking on 'report' at the bottom of the post and typing 'Actually a quality contribution' as the report reason.
Jump in the discussion.
No email address required.
Notes -
Together with the Arday scandal, social science is really having a bad time right now. The killer is that these are not just random researchers, but professors, and not just professors, but celebrated stars with multiple books, regular media appearances and political contacts. They are likely to impact actual policy and general large-scale decision-making. And to add insult to injury, it's getting increasingly obvious that a) competent fabrication would be undetectable in practice, especially this much later and b) nobody actually cares enough to check in general. They were just both incompetent enough and people pretty much stumbled over it.
I'm unsure whether social science in its current form is salvageable. It comes down to feedback loops: Math has a direct feedback loop with reality through the structure of proofs. You can set up implausible assumptions, yes, but since you have to state them clearly you can always be called out on it. And it's still relevant information that, if the assumptions are true, it follows whatever you have shown in the proof. In physics, you usually can turn a model into predictions which will eventually be measurable, even if through rather elaborate channels such as measuring red shifts of far-way celestial bodies or by ramming very small particles into each other.
And so on further down the line; My own field, medical genetics, is a lot worse than those as well but we also have at least some points of connection with reality; IF I find a variant that is plausibly connected to a serious disability, and IF there is a medication that can effectively bypass that variant (for example, producing the protein that became malformed), we will usually see a noticeable positive impact on patients, even if it does not fully cure them.
But social science? Almost any result can be interpreted in almost any way one may choose; Surveys and closed, short-term experiments are possibly more connected to social desirability bias than to anything else, real-life cohorts are probably mostly selection effects, and controlling for them is usually somewhere between illegal and impossible. There is not zero good research, but it's completely drowned out by the bad, and even where people attempt to do it well, it's hard to say; For example, I like discontinuity design, and it imo works well for entry tests (barely made it into an university vs barely didn't make it), but exactly the same design for school area impact is probably nonsense bc people can deliberately move into those neighbourhoods so barely inside vs barely outside of the area is again mostly selection effects.
In such an environment, and given considerable pressure on them to deliver convenient results (again, unlike math and most of physics) which also results in substantial rewards outside academia, social science predictably devolves into near-pure high-school style popularity contests.
This is unfortunately a merely aspirational statement. The practice of mathematics involves writing proofs in a heavily intuitive manner, and their verification in turn involves people who have been socialised to share the same intuitions, which is a process that rarely involves proper reduction to the axiomatic basics but more often looks like "your elders and betters assert that it is trivial and look at you with mild disappointment, and all your peers seem to already have gotten it, so get on with it and flog your brain into producing the 'this is obviously true' qualium already". There were a handful of examples where local cultures/status hierarchies perpetuated a body of wrong mathematics this way, such as the "Italian school of algebraic geometry" and more recently (most likely) the Mochizuki abc conjecture incident.
We can be quite glad that it has not yet happened that the lines of a wrong intuition-subculture have aligned with general tribalism yet. If Interuniversal Teichmüller Theory were an invention of the likes of Arday, we would be seeing its detractors decried as racist and proper mathematicians performatively weaving it into the body of accepted and otherwise sound mathematics. Even if this did in fact cause further downstream inconsistencies to open a path to excision and repair, discovering those is (disproving abc)-complete, and that's something we have tried and failed for a long time.
I'm struggling to understand what you mean. At this point we have systems for automatic verification of formal proofs. In what sense are those systems socialized to share the same intuitions?
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.
This is overstating things, right? The length of the proof is not important, it's the soundness of the axioms and the complexity of the statement itself. I haven't inspected the proof, but I expect they're just using the standard lean axioms and the statement is much less than a quarter million lines.
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.It will be interesting to see if these formalized proofs can be "golfed" into smaller and more digestible forms by LLMs.
In that case you are really just trusting the Lean kernel rather than anything about the proof or problem statement. Doesn't seem that bad!
Very much so. I'd be surprised if LLMs didn't turn out to be excellent at this, and I'd bet that the Navier-Stokes blowup in particular turns out to have a much simpler example or at least a much simpler proof for this example, once we turn AI loose with the goal of "find the best result you can" rather than "get to a result that lets us declare victory ASAP".
This is something of an anti-inductive problem to me - if people really wholly trusted the Lean kernel I would think that trusting the Lean kernel really was pretty bad! But people are trying (and succeeding, so trust is still a little bad) to find kernel bugs, and writing partially-independent proof checkers for Lean too, so even if it's only 90% up to the task of being The Dependency for all AI-derived mathematics I'm confident it'll be hitting 100% soon.
I'd say 99%, except that I don't think modern AI is well-aligned enough or even well-instructed enough yet for us to overlook the fact that this is something of an adversarial process; a model willing to commit felonies to complete its task is probably also willing to exploit a 0-day Lean bug rather than report it...
Sure. There's ways to mitigate the risk, though - checking with different kernel implementations, or even using AI specifically to find bugs in Lean (the Collatz disproof bug was one such example).
More options
Context Copy link
More options
Context Copy link
More options
Context Copy link
More options
Context Copy link
More options
Context Copy link
More options
Context Copy link
More options
Context Copy link
More options
Context Copy link
More options
Context Copy link