pcfwik

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 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 necessarily that useful) to express proofs in a formal logic carefully enough that they could be checked by computers; this was a fringe focus of a minority 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!

Since this is about C declarations: for anyone who (like me) had the misfortune of learning the so-called "spiral rule" in college rather than being taught how declarations in C work, below are some links that explain the "declaration follows use" idea that (AFAIK) is the true philosophy behind C declaration syntax (and significantly easier to remember/read/write).

TL;DR: 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.

https://eigenstate.org/notes/c-decl https://news.ycombinator.com/item?id=12775966

Oh awesome, thanks for the pointer!

I once considered Wren for a situation where I (to a first approximation) wanted to allow users to write 'plugins' that link against my internal C application symbols but using a language focusing more on ease of use (rather than C).

Unfortunately, neither Wren nor any of the other major 'embeddable scripting languages' (e.g., Lua) were really a good fit for this, because they commit fully to the 'all-numbers-are-floats' thing and generally don't seem to even try to provide a general equivalent to the C++ `extern "C" { ... }` thing.

Of course, I know this isn't really the target use case of Wren/Lua/etc., but if anyone knows of a good embeddable scripting language for this I'd love to hear about it. Eventually I went with CPython (which provides ctypes to solve my problem) but it's a huge pain to embed properly.

FWIW --- programmer dvorak lets you type () without "shift" but both ~ and ^ require shift. https://www.kaufmann.no/roland/dvorak/

Re: visualizations of lambda terms, also see "To Dissect a Mockingbird" https://dkeenan.com/Lambda/

makes sense, thanks --- cool project!

Also find it interesting that you're allowing out-of-bounds pointer arithmetic as long as no dereference happens, which is a class of UB compilers have been known to exploit ( https://stackoverflow.com/questions/23683029/is-gccs-option-... ). Do you disable such optimizations inside LLVM, or does Fil-C avoid this entirely by breaking pointers into pointer base + integer offset (in which case I wonder if you're missing out on any optimizations that work specifically on pointers)?

Given the goal is to work with existing C programs (which already have free(...) calls "carefully" placed), and you're already keeping separate bounds info for every pointer, I wonder why you chose to go with a full GC rather than lock-and-key style temporal checking[1]? The latter would make memory usage more predictable and avoid the performance overhead and scheduling headaches of a GC.

Perhaps storing the key would take too much space, or checking it would take too much time, or storing it would cause race condition issues in a multithreaded setting?

[1] https://acg.cis.upenn.edu/papers/ismm10_cets.pdf

To add another suggestion for understanding the Fourier transform, personally the first explanation that ever clicked with me was the Aho/Hopcroft/Ullman algorithms textbook.

Rather than talking about sine and cosine waves, they motivate the Fourier transform entirely in terms of polynomials. Imagine you want to multiply two polynomials (p(x) and q(x)). The key is to recognize that there are two ways to represent each polynomial:

1. "Coefficient form," as a set of coefficients [p_0, p_1, p_2, ..., p_d] where p(x) = p_0 + p_1x + p_2x^2 + ... + p_dx^d, OR

2. "Sample form," as a set of sampled points from each polynomial, like [(0, p(0)), (1, p(1)), (2, p(2)), ..., (d, p(d))]

Now, naive multiplication of p(x) and q(x) in coefficient form takes O(d^2) scalar multiplications to get the coefficients of p(x)q(x). But if you have p(x) and q(x) in sample form, it's clear that the sample form of p(x)q(x) is just [(0, p(0)q(0)), (1, p(1)q(1)), ...], which requires only O(d) multiplications!

As long as you have enough sample points relative to the degree, these two representations are equivalent (two points uniquely defines a line, three a quadratic, four a cubic, etc.). The (inverse) Fourier transform is just a function that witnesses this equivalence, i.e., maps from representation (1) to representation (2) (and vice-versa). If the sample points are chosen cleverly (not just 1/2/3/...) it actually becomes possible to compute the Fourier transform in O(d log d) time with a DP-style algorithm (the FFT).

So, long story short, if you want to multiply p(x) and q(x), it's best to first convert them to "sample" form (O(d log d) time using the FFT), then multiply the sample forms pointwise to get the sample form of p(x)q(x) (O(d) time), and then finally convert them back to the "coefficient" form (O(d log d) using the inverse FFT).

> This is the leverage paradox. New technologies give us greater leverage to do more tasks better. But because this leverage is usually introduced into competitive environments, the result is that we end up having to work just as hard as before (if not harder) to remain competitive and keep up with the joneses.

Off-topic, but in biology circles I've heard this type of situation (where "it takes all the running you can do, to keep in the same place" because your competitors are constantly improving as well) called a "Red Queen's race" and really like the picture that analogy paints.

https://en.wikipedia.org/wiki/Red_Queen%27s_race

I assume the poster is referencing Citizens United v. FEC, specifically about the government's use of the 2002 Bipartisan Campaign Reform Act to restrict showing of political documentaries (apparently, called "Hillary: The Movie" and "Celsius 41.11").

While (as far as I know) the law was never actually used to ban books (only documentaries), the case became infamous because the government argued that it had the right to ban books if it wanted to. See, e.g., the NYTimes article below: "The [government's] lawyer, Malcolm L. Stewart, said Congress has the power to ban political books, signs and Internet videos, if they are paid for by corporations and distributed not long before an election.".

https://www.nytimes.com/2009/03/25/washington/25scotus.html https://en.wikipedia.org/wiki/Citizens_United_v._FEC https://www.law.cornell.edu/supct/cert/08-205

Absolutely not a perfect solution, and maybe you're already using it within your Makefiles, but for anyone who doesn't yet know about it there's Latexmk[1] which is supposed to automate all of this hassle. I think at least on Debian it's included with texlive-full. In addition it has some nice flags like `-outdir` which lets you send all the crazy LaTeX intermediate build/aux files to a separate directory that's easy to gitignore.

https://mgeier.github.io/latexmk.html#running-latexmk

> That is not a TCP/IP stack in 200 LoC.

I agree --- I mostly think it's interesting as one of the most concrete examples of what they claim to have actually done that I've been able to find.

In general, it's frustrating that, as far as I can tell, they don't seem to have made any of the code from the project open source. Widespread skepticism about their claims due to this is (IMO) justified.

(Edit: for folks interested, it seems like some of the code has found itself scattered around the Web ... https://news.ycombinator.com/item?id=19844088 )

> I don't think they DID build a modern computing environment at all.

I agree that, now, after they've tried and failed, we can say they didn't build a modern computing environment in 20kloc.

My point is just that, when they were pitching the project for funding, there was no real way to know that this "trillion dollar technology" goal would fail whereas nukes/moon mission/etc. would succeed. Hindsight is 20/20, but at the beginning, I don't think any of these projects defined themselves as "doing something that lots of people are trying to do all the time;" instead they would probably say "nobody else has tried for a 20kloc modern computing system, we're going to be the first."

Given they all promised to try something revolutionary, I'm not sure it's fair to claim after-the-fact how obvious it is that one would fail to achieve that vs. another.

But I do take your point that it's important in general not to fall into the trap of "do X but tweak it to be a bit better" and expect grand results from that recipe.

Sorry, added an edit to my above post before I saw this, just to summarize:

I think that's a more reasonable complaint, but I fear it's too vague to be applicable.

The STEPS folks would probably say that a modern computing environment in ~20kloc is something that was previously unaccomplished and thought to be unaccomplishable, but you're writing that off/not counting it as such, presumably because it failed.

On the other end of the spectrum, things like Git (to my knowledge) did come out of the "find a better way to source control" incremental improvement mindset. (Of course, you can say the distributed model was "previously unaccomplished," but the line here is blurry.)

> Let me guess, they published a bunch of papers, did a bunch of experiments like "lets do X but gui" "what if you didn't have to learn syntax" and then nobody ever did anything with any of the work because it was a total dead end.

This response is very confusing to me, and it seems you have a very different understanding of what STEPS did than I do.

In my understanding, the key idea of STEPS was that you can make systems software orders of magnitude simpler by thinking in terms of domain-specific languages, i.e., rather than write a layout engine in C, first write a DSL for writing layout engines and then write the engine in that DSL. See also, the "200LoC TCP/IP stack" https://news.ycombinator.com/item?id=846028

You seem to think they're advocating a Scratch-like block programming environment, but I'm not sure that's accurate. Can you point to where in their work you're finding this focus?

I too believe STEPS was basically a doomed project, but I don't think it's for the reason you've said (moreso just the extreme amount of backwards compatibility users expect from modern systems).

(--- edit: ---)

> You don't make leaps from paying grad students to play around with "how can we make programming better", you get it from all of a sudden an AI can just generate code.

I think this is a more compelling point, but it doesn't seem to explain things like the rise of Git as "a way to make programming (source control) better," and it's not clear how to determine when something counts as an "all of a sudden" sort of technology. They would probably say their OMeta DSL-creation language was this sort of "all of a sudden" technological advance that lets you do things in orders of magnitude less code than before.

I think it would get a lot less hate if Google just made it possible to opt-out of them without having to download some third-party browser extension (which is actually what Google's AI summary itself suggests I do when I ask it how to turn itself off!). A small "opt out" link on the top of the AI suggestion would make most of this hate go away, and would make me stop paying for Kagi, if Google cared.

I also find it extra frustrating when AI summaries appear when I search for correctness-critical information, e.g., "what temperature to cook chicken?" or "can I eat old eggs?" --- why force me to scroll past an entire page of AI generated, 1%-chance-of-being-a-literally-lethal-hallucination "summaries" in order to find the CDC's actual recommendation? I don't want to play Russian roulette with my health hoping I don't get a hallucination, instead I just want the authoritative answer. Which Google did an amazing job at until a year ago, and Kagi is doing a pretty great job at now.

This book has some nice cuttable flexagon templates on thicker paper, with designs: https://www.amazon.com/Fantastic-Flexagons-Hexaflexagons-Oth...

The designs are fun, although I find that the thicker paper actually makes them a bit harder to fold and flex than typical printer paper.

If you find flexagons interesting, you might like trying to find a copy of Martin Gardner's "Scientific American Book of Mathematical Puzzles and Diversions" at your local used book sale. The first chapter is about flexagons and it gets better from there! Wonderful car ride, plane, etc. distractions.

https://www.amazon.com/Scientific-American-Mathematical-Puzz...

At least in my personal case: GLR sounds great in theory, but I like to implement things 'from scratch' when possible. Both PEGs and the basic Earley algorithm are incredibly simple to write up and hack on in a few hundred lines of insert-favorite-language-here.

GLR would probably have (much) better performance but I'm usually not parsing huge files (or would hand-roll one if I were). I've not yet found an explanation of GLR (or even LR for that matter) that's quite as simple as PEGs or Earley (suggestions welcome tho!).

There was an interesting discussion two years ago regarding nonobvious issues with PEGs:

https://news.ycombinator.com/item?id=30414683

https://news.ycombinator.com/item?id=30414879

I spent a year or two working with PEGs, and ran into similar issues multiple times. Adding a new production could totally screw up seemingly unrelated parses that worked fine before.

As the author points out, Earley parsing with some disambiguation rules (production precedence, etc.) has been much less finicky/annoying to work with. It's also reasonably fast for small parses even with a dumb implementation. Would suggest for prototyping/settings when runtime ambiguity is not a showstopper, despite the remaining issues described in the article re: having a separate lexer.