Paracompact

> The toxicity comes from the intellectual profession having to function as a modern clerisy for socioeconomic reasons under post-neoliberal capitalism.

Sure. And I think (Western, post-neoliberalized) math has resisted that corruption possibly better than any of its sibling cultures. But what makes the toxicity "distinct" is the emphasis on enlightenment, as if being a top-class mathematician brings you closer to the Godhead than does, say, being a top-class chess player, or a top-class defense attorney. Mathematical theories are treated less like robust human creations percolating over decades and more like divine revelation channeled through chosen disciples in fits of inspiration (c.f. Cantor, Galois, Godel, Grothendieck). A lot of this is projected from the outside the culture into it, but it is not outright rejected by the culture. Instead we still openly endorse what amounts to Great Man theories of mathematical history, attributing to almost every noteworthy mathematician a moniker of "genius" and praising them as paragons of thought, not as the unhealthy subjects of cults of personality.

n.b. I think math culture is probably one of the least toxic cultures that have ever existed. Its equanimity and principles are a big part of what drew me to math in the first place. But humans are human.

Do you know why it's easier to specify theorems than it is their proofs? Or why ACSL != C?

You can go ahead and make a more specific argument, e.g. that mainstream UX-centric software development may not be amenable to current paradigms of formal verification, but to insinuate that a complete spec reduces to source code itself is naive.

My confidence in the validity of their claims tanked right about here.

I'm all for regulating transparency into social media algorithms. Meta most certainly is compromised by foreign actors. But can we choose less stupid hills to die on than numerology and GIFs? Headline is not remotely supported by the evidence.

Devil's advocate here: Why is having many possible implementations a bad thing? Sure, you don't want to half-ass your specifications and fail to pin down your product properly, but if you do pin down what matters, then by definition what remains is discretionary. Formal specs (e.g. the C spec) behave the same as informal specs in this regard.

The real question is whether humans in an agentic workflow can actually identify all of what's structurally and functionally necessary for their product. Either the spec writer must be expert, or the agent must be savvy enough to identify and collaborate with the non-expert. Right now, agents like to just plough through underspecification or bad ideas so that they can deliver as quickly as possible.

Hacking websites and submitting false police reports.

Going back to C++ would be particularly bizarre to me given that AI is also very proficient at verified languages. Not merely typesafe, but languages comprising their own spec languages such as Rocq and Lean.

I predict that in the next decade: (1) the market will understand the difference between a "code writer" and a "spec writer," with (2) the expectation that the latter is overwhelmingly more necessary than the former in an AI-dominated field, and (3) there will emerge more useful and less mathematically specialized formal verification alternatives to Rocq and Lean, and a filling-out of the tooling gap of between "static typing" and "interactive proof assistant," perhaps in the vein of ACSL-like contract annotations, and (4) there will be a subsequent shift in the traditional curriculum for programmers. Since educational change is slow (and spec writing depends on good coding fundamentals anyway), perhaps (4) is a stretch, but I'm more confident in the first three.

Where does this myth come from, and how does it survive? It's either an excuse for parasitic corporatism, or an expression of learned helplessness. Nobody has been successfully sued for prioritizing the long-term health and reputation of a company over self-starving quarterly profit.

Is there a perverse incentive toward the latter anyway? Yes. But it mostly serves current leadership, who are evaluated and paid on short horizons, at the expense of the long-term investors who own most of the equity.

Eh. I'm a math PhD who fled academia because it was too much for me. But I have never encountered this term "abstraction ceiling" nor did I succumb to it. I simply ran out of motivation to pursue higher math, especially when following through on learning and research became more and more labor. (It was always labor; but it was a labor I used to love.) I am far from a prodigy.

> even epsilon-delta proofs are enough to eliminate the majority of the population, no matter how good a teacher you are

Disagree. It's a notoriously hard subject to teach, and with all the demands placed on e-d in so little time in your average curriculum, it doesn't require appeals to IQ to explain its infamy. With enough motivation and practice, the quantifier alternation is comprehensible to any sound mind. What your average mind (and student) lacks is exposure to formalism, abstraction, and how these things tie in with what they are familiar with, which is symbolic manipulation. With the exception of geometric proofs (another educational bugbear), they have little context for what formalism is or why it matters.

Not only that, but there is a very fuzzable tell of something funny in the Collatz proof script (`CommandElabM`, i.e. metaprogramming). We may not at all be so lucky in other malicious scripts, especially if there are still kernel-level bugs in Lean.

The fear is not that they will just slow down progress for all. It is that regulation will specifically burden competition. If you kill open-source training, ban Chinese models, crack down on self-hosting, grandfather OpenAI/Anthropic/Google into regulatory compliance while throwing the book at startups, etc. you wind up in the worst of all possible worlds.

At this point in time, we really can't be confident in accepting proof certificates without any human eyes on the script that generated it. I still have 95%+ confidence in this particular result being trustworthy, but a precedent of blind faith is guaranteed to end badly.

Do you believe no open questions remain as to the truth of the Collatz conjecture?

Second of all, you did not read the link.

> In particular, we use honest when the goal is to create a valid proof. This allows for mistakes and bugs in proofs and meta-code (tactics, attributes, commands, etc.), but not for code that clearly only serves to circumvent the system (such as using the debug.skipKernelTC).

Given that AI has autonomously found proofs of `False` in Lean and other proof assistants, it is far from impossible that such a circumvention could be present somewhere in 13 million lines.