porcoda

More specifically, a combination of mathlib (human, expert curated) and projects like TauCeti (AI-welcome complement to mathlib). See: https://github.com/TauCetiProject/TauCeti

As others said, it's not that this isn't a phenomenon that is unique to now. It happens. I had to pivot a bit of my dissertation near the end because at a random conference I spoke with a researcher from another continent and realized one of my ideas was already out there in some form. I just missed it since it was in a conference proceedings outside the usual set I looked at. So, I had to scramble to adjust and still come up with something novel. I survived, and defended, but it wasn't that much fun at the time.

What isn't so normal is the probability and ease by which this kind of thing can happen today versus decades ago when I was in school. As OpenAI said, it only takes a few hours of compute to do what likely was much more than a few hours of human effort. The only reason this kind of scooping/overlapping was rare was mostly a function of how fast other humans could do the same work. With machines, that totally changes the relative pacing between the human trying to learn how to be a researcher and the machine that can grind out results.

I'm less worried about the phenomenon of overlap and scooping and such. I'm more worried about the long-term impact on fields (not just math), especially considering the early stage students and researchers entering the pipeline now. I'm not sure what happens to disciplines when that pipeline stalls.

They aren't, but the problem is that open problems tend to emerge when people are working on other problems. If fewer people are spending time deeply thinking about current problems since a handful of labs are solving them with AI without an eye towards understanding and only on verification, the pool of open problems won't be continuously growing. There is a fear that there will be a chilling effect on the community if people are disincentivized from trying to solve deep problems or study them for understanding as opposed to simply focusing on verification. It's more of a social and community problem than a fundamental problem with mathematics itself becoming "completed".

That would be a great outcome of this situation. I doubt it will happen though: unlike fuel efficiency rules, there aren’t likely to be external pressures like that on software. Outside developer circles most users likely are unaware of memory usage and often just accept that computers are slow and unreliable sometimes. That’s different from drivers who see their fuel gauge and the corresponding cost of fuel, and are thus very aware of what fuel efficiency means.

I think mlton is the one to reach for if you want strict conformance to the SML'97 definition [1]. There's a page on the MLton site that describes where SMLNJ deviates from SML'97 [2].

I'm surprised Gemini says SML/NJ its the most widely used. I've been an active Standard ML user for close to 30 years, and while that was certainly true for the first half of that time, I found most projects around me drifted to defaulting to want to compile with mlton or polyml. SML/NJ's heap2exec was a bit clunky compared to the others. It's great that they're slowly moving it over to LLVM.

[1] http://www.mlton.org/Features

[2] http://mlton.org/guide/20051202/SMLNJDeviations

For those interested in the Standard ML compilers, Mlton is another one worth checking out. Standard ML of New Jersey (smlnj) is another interesting one although it tends to be more of a research vehicle than polyml or mlton. If you are inclined toward verification, the cakeml project is quite cool as well. For those unfamiliar with standard ML, if you’ve heard of ocaml or F#, they’re relatives in the ML language family.

I am eager for a lean equivalent of flocq in rocq. When I did some lean verification of numerical algorithms I did the same thing with rationals or the reals from mathlib. The big gap between that and the actual code is the lack of a solid theory library to pull in that would give me IEEE floats that is at the same level of quality as Flocq. I’m eager for that to come along (unless it has and I just haven’t found it yet).

I use it a few times a week for about that long, almost exclusively as a virtual display for my MacBook. I bought it mostly because I travel for work, and when I'm stuck in a hotel and want to work I wanted something similar to my big screens at home. It's also nice to be able to kick back and watch big screen movies or TV on travel too. Long usage is fine for me - with the inserts I have my computer glasses prescription so things look good.

NSF is one of the primary agencies supporting research in the US. It’s not a “foundation” in the sense of charitable foundations if that’s what’s confusing you about their name. The base research engine that fuels the US in most disciplines comes from support like NSF, DOE, NIH. Damage those, and you damage the foundation upon which a lot of our intellectual strength sits.

Not really surprising. I would guess this goes beyond just the AI and jobs issue. Your average person sees AI all over the place in contexts they didn’t ask for it but can’t escape. Social media is covered with AI garbage (e.g., AI generated videos). Podcasts are being flooded with AI garbage that are pretty overt grabs for ad impressions where quality is … not important. Appliances and consumer devices are getting AI that nobody asked for. And of course, our world of tech stuff where the selling point is more or less leaning hard into FOMO (“Everybody’s doing it - don’t you want to be an 100x developer and not get left behind?”).

It’s easy to fixate on the OpenAI and Anthropic-level companies, but the real inescapable flood of AI garbage is coming from the downstream companies building on the core AI providers. Communities like HN have some role to play here. Maybe some peer pressure on AI founders to, maybe, not make the world a worse place?

As others pointed out, the explosion of interest started with the deep convolutional networks that were applied in image problems. What I always thought was interesting was that prior to that, NNs were largely dismissed as interesting. When I took a course on them around the year 2000 that was the attitude most people took. It seems like what it took to spark renewed interest was ImageNet and seeing what you get when you have a ton of training data to throw at the problem and fast processors to help. After that the ball kept rolling with the subsequent developments around specific network architectures. In the broader community AlexNet is viewed as the big inflection point, but in the academic community you saw interest simmering a couple years earlier - I began to see more talks at workshops about NNs that weren’t being dismissed anymore, probably starting around 2008/09.

Yup. The rumor mill was talking about a CEO change for a while, and around the time you saw the rumors building you saw the departures you mentioned. Ternus was being mentioned as the likely successor at least back to November last year. So internally the shifts have already been happening for some time, only observable on the outside via the high profile departures.

I’ve had similar experiences with code I’ve proven correct, although my issues were of the more common variety than the overflow issue - subtle spec bugs. (I think the post mentions the denial of service issue as related to this: a spec gap)

If you have a spec that isn’t correct, you can certainly write code that conforms to that spec and write proofs to support it. It just means you have verified a program that does something other than what you intended. This is one of the harder parts of verification: clearly expressing your intention as a human. As programs get more complex these get harder to write, which means it isn’t uncommon to have lean or rocq proofs for everything only to later find “nope, it has a bug that ultimately traces back to a subtle specification defect.” Once you’ve gone through this a few times you quickly realize that tools like lean and rocq are tricky to use effectively.

I kinda worry that the “proof assistants will fix ai correctness” will lead to a false sense of assurance if the specs that capture human intention don’t get scrutinized closely. Otherwise we’ll likely have lots of proofs for code that isn’t the code the humans actually intended due to spec flaws.

In my experience over the last couple years, lists like this won’t move the needle at all. The AI zealots reject anything that calls into question the AI stuff, usually appealing to “just wait, better models/agents/guardrails imminent” and claiming that anecdotal productivity gains are worth the risk. The people concerned about AI already are concerned and just fall back to “I told you so”. Unfortunately the decision makers seem to still be following the zealots promising wondrous productivity, profit, and a future full of flying cars.

Effective April 20? Sometimes these days it’s hard to distinguish reality from The Onion.

Interesting how not many comments talk about the game itself and how Epic may have driven their own players away with changes that players dislike. I’ve played for most of the life of the game pretty regularly and I’ve found myself growing tired of “yet another season full of movie/TV crossover junk”. You can tell they’re focusing on pulling money in via partnerships, and not paying much attention to “is this what players want”. Unsurprising you’d see player numbers drop.

I work in a subfield of CS that requires those fundamentals pretty regularly, and I also make regular use of AI tools. You definitely need those fundamentals because AI tools can’t always be trusted to make good decisions when it comes to them. Knowing the fundamentals yourself is critical to keep the AI assistants in check, both to know how to guide them AND to know to recognize when they made a bad decision.

A recent example for me: I had a challenging problem in a medium sized codebase (tens of thousands of lines) that boiled down to performing some updates to a complex data structure where the updates needed to be constrained by some properties of the overall structure to maintain invariants. Maintaining the invariants while the data structure was being updated is tricky since naive approaches would required repeated traversals of the whole structure. That would be really inefficient, and a smarter approach would try to localize the work during the updates. The latest Claude and GPT assistants recognized this, but their solutions were exceptionally complex and brittle. I eventually solved it myself with a significantly simpler and more robust method (both AIs even gleefully agreed that my solution was slick after I did it).

Had I let my CS fundamentals go to waste I wouldn’t have been able to solve it myself, nor would I have been able to recognize that the solutions posed by the models were needlessly complex.

Just because an AI can generate a solution that passes tests quickly doesn't mean what it generated is a long term good solution. Your skills in fundamentals is key to recognizing when it does a good job and when it doesn’t, and being able to guide it in the right direction.

They define this:

“The influencers presented their claims as exposés of industry deceit, despite offering no verifiable evidence to support them.”

So, misinformation = make claim with no supporting, verifiable evidence. Seems like a pretty standard, neutral definition.

> Absolutely not. Reading a language is crucial.

I don't think the post implied that this package writing activity was a write-only activity where reading and learning is strictly forbidden.

> You can find open source licensed packages, read them to understand them, and then copy them into your config. Doing everything from scratch is a waste of time unless you enjoy the process (in which case go nuts).

The post clearly indicates the relatively large set of open source packages they looked at and understood before doing their own packages. The author graciously acknowledges them and their influence on the work:

"Emacs Solo doesn't install external packages, it is deeply influenced by them. diff-hl, ace-window, olivetti, doom-modeline, exec-path-from-shell, eldoc-box, rainbow-delimiters, sudo-edit, and many others showed me what was possible and set the bar for what a good Emacs experience looks like. Where specific credit is due, it's noted in the source code itself."

Not really a new term: “warfighter” always has made me cringe but it’s been commonplace in defense contractor pitches to DoD for many years. Basically, if you hear it being used you’re likely in the presence of someone who does (or did) DoD work. Totally unsurprising to see it here given this is a DoD contracting argument that we’re all watching from the sidelines.

I noticed the same thing, having also written an interpreter for the Wolfram language that focused on the core rule/rewriting/pattern language. At its heart it’s more or less a Lisp-like language where the core can be quite small and a lot of the functionality built via pattern matching and rewriting atop that. Aside from the sheer scale of WL, I ended up setting aside my experiments replicating it when I did performance comparisons and realized how challenging it would be to not just match WL in functionality but performance.

Woxi reminds me of some experiments I did to see how far vibe coding could get me on similar math and symbolic reasoning tools. It seems like unless you explicitly and very actively force a design with a small core, the models tend towards building out a lot of complex, hard-coded logic that ultimately is hard to tune, maintain, or reason about in terms of correctness.

Interesting exercise with woxi in terms of what vibe coding can produce. Not sure about the WL implementation though.

(For context, I write compiler/interpreter tools for a living - have been for a couple decades)

The em-dash metric is silly. Some people (including me) have always used them and plan to continue to do so. I just pulled up some random articles by Wolfram from the before-LLM days and guess what: em-dashes everywhere. One sample from 2018 had 89 of them. Wolfram has always written in the same style (which, admittedly, can be a bit self-aggrandizing and verbose). It’s kinda weird to see people just blowing it off as AI slop just because of a —.

Yes. This is one of the things that drives me nuts about a lot of titles on here: the context like “for the web” changes how it’s is interpreted a great deal. I see the same thing when I see posts about other languages and AI and such. Context matters versus making it sound like a broad, general statement. Alas, the broad, general statements likely get more engagement..

This seems like a business opportunity. “Ethically sourced organic mud speaker wires for a clean, organic, pure sound.” /s

The footnote on their sentence about assembly programmers: “I mean, I dunno. I'm not a historian. This is a vibes-level historical reconstruction. I would be curious if this is way off base though”

So, yeah. They just made it up because it felt right. (Which, I guess is what one would expect from AI related stuff these days.)

You’re definitely right though: it doesn’t take a deep dive into the history of computing and programming languages to find higher-than-assembly level languages emerging at the very dawn of computing.

> At the end of the day, I am a Builder. I like building things. The faster I build, the better.

This I can’t relate to. For me it’s “the better I build, the better”. Building poor code fast isn’t good: it’s just creating debt to deal with in the future, or admitting I’ll toss out the quickly built thing since it won’t have longevity. When quality comes into play (not just “passed the tests”, but is something maintainable, extensible, etc), it’s hard to not employ the Thinker side along with the Builder. They aren’t necessarily mutually exclusive.

Then again, I work on things that are expected to last quite a while and aren’t disposable MVPs or side projects. I suppose if you don’t have that longevity mindset it’s easy to slip into Build-not-Think mode.

I’ve done both Swift and rust for Linux applications (symbolic analysis tools and compilers, not web stuff or other server apps). I have to say, I’m torn after building a couple moderate (10-30k SLOC) scale tools in both. I prefer swift since I feel like I’m working at the abstraction level I prefer and letting the ARC stuff take care of memory for me. Rust isn’t so bad, but it does make me think more about things that I don’t when I’m in Ocaml or Swift. Rust has better tooling: the LSP support makes life nice in emacs. Compiler feedback and clippy : super useful. Not a fan of the high usage of crates (I’m in the paranoid about supply chain camp). Swift felt like it shipped with more batteries included. I think the main factor is the people side: however much I like swift, I’m more likely to find rust people in my world. I’m rooting for swift though: the world has room for more than one memory safe C++ successor.

In their revenue report this week out of $140B, services made up 30B. 140B-30B = 110B. Thats pretty far from bankruptcy.

Nah, it’s just Wolfram being Wolfram. He was generating this scale and style of content well before LLMs were a thing. He usually has some interesting ideas buried in the massive walls of text he creates. Some people can’t get past the style and personality though (I can’t blame them…).

I’m glad to see people finding coding accessible again. To me this kind of common “AI made coding fun and accessible again” message signals something deeper. As a field, we allowed our systems to get so complex that we lost people: and AI tools are bringing them back. Maybe we should look at how we have chosen to design systems and say “can these be made simpler and more accessible”? Even before AI systems I looked at my field with sadness: there is complexity growing everywhere and few people looking to address that. Instead, we seem to have incentivized creating complexity because new complicated systems that are hard to use lead to career advancement if you can point at something and say “I am one of the few who can deal with that” or “I created that complex thing”. The ability to handle the complexity makes an individual valuable even though the effect is it excludes many others.

Perhaps if we didn’t have deep layer cakes of frameworks and libraries, people would feel like they can code with or without AI. Feels like AI is going to hinder any efforts to address complexity and justify us living with unnecessary complexity simply because a machine can write the complex, hard to understand, brittle code for us.