pcfwik

It's actually still accessible from computers on the local Stanford network, so someone could probably forward you a copy of whatever you're looking for. CS department affiliates recently got an email about other sites on the cs.stanford.edu subdomain not being accessible from off-campus. That email included a note "Our team is aware of the issue and is actively working toward a solution to restore access for off-campus". Unsure if it's related to recent vulnerabilities, but it wouldn't surprise me.

Separately, I know Knuth has recently mentioned drowning under a sea of (presumably LLM-found) bugs in TAOCP, so I suspect it might lead to a slight (if accidental) reprieve :)

If I understand correctly, one of the recent cool generative AI-assisted results is actually supposed to have closed this problem, complete with a Lean proof!

https://arxiv.org/abs/2608.29592

If this suggestion were to come to pass, I wonder how new math PhDs would think about choosing between a 'normal' R1 faculty job vs. the "teaching route" (teaching professorships, lectureships, community college professorships, or SLAC professorships).

It's been my understanding that traditionally the ones who care about "motivated explanations" in this sense go for the latter, but if the research community has now decided they care about teaching and understanding, it might "even the playing field" and make the jobs more similar.

Agreed that logic isn't a branch of mathematics (even today, my experience has been that logic classes tend to be offered by philosophy departments, not math). My only quibble was the implication that logic is somehow much newer than mathematics (/Euclid). It's not like people suddenly woke up one day in the 20th century and thought for the first time: "huh, I wonder what separates correct arguments from incorrect ones?" But point taken that Aristotle was not as formalist in his time.

If you have some sources to read more about this:

> I get the impression that a lot of more traditional philosophers of logic hated the formal turn.

I would be very interested! (Don't doubt it at all, just sounds like an interesting period I don't know as much about as I'd like.)

I broadly agree with your sentiment and am saddened (outraged?) to see the financially-motivated cheapening of (destruction of?) what mathematics truly is. I agree that formal logic is merely a model of one aspect of what mathematicians do, in the same sense that a computer simulation of a roller coaster can never bring the same value to us as the real thing.

However, I would be remiss if I didn't question your historical claim, which seems to me a bit too strong:

> Mathematics predates the idea of formal proof by millenia [...] Formal proof only emerged early in the 20th century [...]

You seem to associate the start of "Mathematics" with Euclid, but (as far as I know) he worked at approximately the same time as Aristotle. Aristotle's syllogisms are perhaps the most famous formal logic system: their correctness relates only to their form, not their content. All deductions of the form "All X are Y, All Z are X, hence All Z are Y" are valid (assuming the premises are), regardless of the meanings of X, Y, and Z. (Outside of Greece, my understanding is that a few hundred years earlier Panini had also developed a system of formal manipulations, but for representing grammars.)

What, to my understanding, "emerged" only the 19th and 20th century was 'merely' a formal logic both expressive and sound enough to properly express modern mathematics (the Beggriffsschrift in the 19th century and FOL+ZFC in the 20th). Between Euclid and the 19th century the development of calculus (17th century) was probably the biggest advance in mathematics, and my understanding is that Leibniz himself spent significant time working on formal logic.

Perhaps I have the wrong definition in mind of 'formal logic' or 'mathematics,' but I do think the history of formal logic is much more closely tied to the history of mathematics than your post makes it seem on first glance. Though I certainly agree that "mainstream mathematics" has never felt it necessary (or even, for the most part, particularly useful) to express proofs in a formal logic carefully enough that they could check by computers; this was a fringe idea from a sub-group of mathematicians and computer scientists that was co-opted as a marketing stunt into 'what mathematics is' for major corporations trying to justify their money burn.

It's never clear what's "real" vs. marketing for the LLM companies, but Mozilla at least has made a big deal publicly about the "unprecedented" number of "latent security bugs" they've found using tools like Mythos:

https://blog.mozilla.org/en/firefox/privacy-security/ai-secu...

https://hacks.mozilla.org/2026/05/behind-the-scenes-hardenin...

To be honest, I'm not sure how many (if any) of them have actually been exploited, but in any case, it seems like the cost to at least find a vulnerability anymore has really dropped dramatically.

Knowing some folks that work on "major-browser-vendor" security in the era of Mythos-found-and-exploited vulnerabilities everywhere, the thought of running completely random untrusted Javascript on my machine has freaked me out to the point that I run NoScript on all of my machines now.

I've found NoScript actually very usable, as long as you allow yourself to be fairly liberal in marking domains "trusted." I only truly routinely visit a core 10-20 domains that require Javascript, and they're from "reputable" organizations (my bank, employer, etc.) so those all get marked "trusted" quickly and I don't worry about them going forward.

In the "long tail" of random things I click on from HN links, seeing a "You need to enable Javascript to view this app" message is actually a fairly good signal that I don't want to view that app (though you might be surprised how many websites are browsable comfortably---or even more comfortably!---without JS enabled).

One thing I wish NoScript supported was the ability to mark a domain as a "trusted page domain" in the sense of: "HTML served from this domain can load scripts from any domain" (rather than trust being assigned to the domain serving the script itself). Perhaps it has this feature and I just haven't found it.

https://noscript.net/

Also very out-of-date, but https://wiki.haskell.org/Regex_Posix#Results_and_Bugs "names and shames."

I think this is a valid point. I would much prefer if the spiral rule were presented as a helpful mnemonic for remembering C operator precedence rather than something uniquely connected to declarations!

Being taught this rule in undergrad really hampered my appreciation of C. As I've said in a previous comment, the real key that unlocked understanding C declarations for me is the mantra "declaration follows use." You declare a variable in C in exactly the same way you would use it: if you know how to use a variable, then you know how to read and write a declaration for it. Once I understood this elegant idea, it became hard to enjoy using statically typed languages that eschew it.

It is explained in more detail at this link: https://eigenstate.org/notes/c-decl

> When I was in mathematics, reading other people's work was always more rewarding to me than doing my own. [...] I really welcome the omniscient mathematician machine people are predicting.

Curious, as someone who relates strongly with both the OP and your first sentence: did it matter that you were reading "other people's work?" Or was it simply the satisfaction of understanding an answer?

Personally, one of the things that finally drew me to math as an undergrad (vs. high school where I thought of it as a stupid competition played by people who cared too much about showing off their smarts) was an instructor who helped me think of studying math as a conversation with a fellow human being many miles, centuries, languages, and cultures removed from me. Despite that distance, my mind was appreciating a creation that another human had cared for and poured years of their life into. There was a sort of romance to it, like the feeling of butterflies-in-the-stomach we get from seeing a multi-thousand-year-old cave painting, yet even more impressive because of the depth of the thought communicated.

I personally haven't been able to recreate that feeling from computer-generated math. Whenever I try to, I feel deeply uncomfortable (somewhat similar to the thought of eschewing human connection for an 'AI companion').

I'm more optimistic than the OP, especially when I think of new discoveries in healthcare. And I know there's enough "organic human-created math" from the last ~2k years that folks who feel the way I do can spend the rest of our lives studying only that. But it is sad to think that this multi-thousand-year project of "communicating human mathematical creations through time" has just ... ended? Or seems to be ending soon? Or at least greatly cheapened from a romantic dream into a sort of fun hobby, like recreational knitting? I can't help but share the OP's sadness that something seems to have been lost for future generations. Though a lot has been (and will be) gained as well, for sure!