Paracompact

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.

After years of using the things, I believe not enough focus is given to high-velocity uses of proof assistants for prototyping. They can altogether replace scratch paper for fumbling around with new concepts.

It's objectively very difficult and technical, it's spatiovisual, it's artistic, learning resources for it are sparse and most just learn by the FAFO method, current AI sucks terribly at it, and it's not likely to ever be specifically targeted by benchmaxxers.

I was using an AI to help me set up a container to be used as the Nix build environment for another AI. This build environment would not have Internet access. I was having it base its approach off a previous container used for a Stack build environment.

In its initial analysis of my proposed strategy, it insists as its premier point /against/ the strategy, "you will have to rebuild the container every time your flake.nix changes."

Two head-slapping errors of judgement in saying something like that:

(1) The Stack solution is identical. Change stack.yaml, the container must rebuild. (2) It is not physically possible to do better than this while insisting on an internet-free environment.

So on this point, it was just parroting advice irrelevant to the context at hand. LLMs always have such a bizarre mix of technical knowledge and lack of good judgment.

And don't even get me started on tricyclics or MAOIs... no, seriously, don't get me started on them! The current generation of first-line antidepressants (SSRIs/SNRIs) might as well be free compared to the old school crazy pills.

IIRC he has expressed support in the past for attempts to formalize IUT in Lean, but we'll see where that really goes, because he's absolutely not clearheaded enough to lead such a project himself.

1. We tend to believe "more power/knowledge/choices" is universally a good thing; that we are rational creatures in some sort of game theoretic landscape where we are free to optimize for our own outcomes, and extra options or information can only be to our optimization benefit.

2. We tend to believe that as moral agents, we have obligations to Good. More specifically, knowingly choosing against Good should in proportion produce Guilt.

The bind that results from (1)+(2) is distinctly Christian to me, obsessed as Christianity is with the notion of shame as a moral whip. It is an exercise in religionmaking how to structure one's psychological incentives so that solipsism is avoided while not sacrificing (1).

It's so very clear why he thought it was a good idea to have a regex validator to check that he doesn't imply he still works at Github.

"i dont work at github"

"Yes, you're absolutely right. I apologize for the mistake and have edited the document accordingly.

reads War and Peace system prompt

Here is how we can programmatically and scientifically avoid this problem in the future:

1. Add to the regex validator library: We can add to the regex validator library an additional entry to catch any future instances of this mistake. This is a low-cost, high-yield approach---regex runs with deterministic and repeatable results, with the added benefit that its big-O runtime scales at most linearly with the size of the text for most use cases (Hartmann, 2018).

*Three other braindead ideas*

Which future-proofing strategy shall we take?"

"sure 1"