porcoda

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.

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.