> we are living through a period of time where success is very hard to define, much less attain.
Do you think this has changed from say 10 or 20 years ago? To me, I don't get the sense that there has been shift in the social definition of success. Maybe I'm missing something?
> Do you think this has changed from say 10 or 20 years ago?
Yes, I do.
The goal is roughly the same: financial security, a good home, as much of a family as one cares to raise.
But for basically my entire life as a middle-aged American, there was a well-lit path to that goal:
1. Do good in high school.
2. Go to a university and get some four year degree. Obviously some degrees are duds, but basically any of them was considered a worthwhile investment.
3. Get a white collar job doing something intellectual. Make a decent salary at a stable company. Change jobs periodically as needed.
Now:
1. Doing well in high school is still important, but it is very easy for kids to get good grades using AI while not actually learning anything and not realizing they are setting themselves up for hardship.
2. College is so expensive now that determining which college and which degree is actually a sound financial investment is very hard. An 18 year-old-kid is being asked to make a financial choice with life-long consequences at a point when they have none of the expertise about their long-term goals to know what to do.
3. AI will very likely eliminate many of these jobs. People will be competing for fewer and fewer jobs and who knows what on your resume will actually help you stand out? Also, most of the blue collar jobs are already gone, either automated away (ag) or moved overseas (manufacturing).
There was also a sense in the US that even if the government wasn't great, it was at least functional and a source of relative stability run by somewhat mature adults. That is clearly no longer the case at the federal level.
What's different is that people who thought they were basically on the "golden path" suddenly have no idea what their job looks like in five years or if it exists.
I agree for SWE specifically that AI is changing the career dramatically, and in a way that makes life less predictable. But I don’t know how the definition of success has changed - at least in America it still seems to be good professional job plus family.
Maybe spell it out in more detail? Forgive my inability to follow the argument.
My overall point is that what's happening in SWE right now is not happening (yet?) in other fields. And so we can't extrapolate from SWE experience to wider social experiance.
AI threatens to obliterate white-collar work entirely (whether it'll actually play out that way it's a possibility constantly talked about by executives and in the news), and that would plunge previously secure people into precarity. The idea this only applies to software engineers isn't true either.
Is there a citation for the decline in third spaces? I read such a claim often. But in my part of the US (Brooklyn NY) the number of third spaces like coffee shops and pottery studios is booming.
When I was a kid kids used to just hang out. We'd take a bus, ride bikes, or walk to the mall, the park, the woods, fast food restaurant, record store, dollar store, etc and just loiter. Nobody had any money to buy anything, but boy we'd browse and loiter. Sometimes we'd just walk for hours. We'd walk miles and miles and miles just to sit at a table at Burger King with a single small fry between our group and hang out there.
Children don't do that anymore; they basically don't leave the house because they have the Internet. They communicate through texting and Discord so they don't even have to "hang out." Beyond the social change, when I was a young adult most malls went 18+ (unless accompanied by parents/guardians) and most other businesses nowadays allow teens to loiter the way we use to. Businesses want people in and out once they are done.
Even if business allowed it, most parents don't allow their kids to leave the house unattended anymore.
You were downvoted but you are correct. Some classic examples of third spaces are English pubs and Dutch coffee houses.
That third spaces include commercial spaces does not imply that “free” (tax or donation funded) third spaces should not exist. Parks and museums are also great third spaces.
While in many countries cafes and pubs served as real third places in the past, rising rents (and other costs) have led many establishments to discourage people from lingering. At my old haunts, loud music is now played to get customers moving on, and the very second you're done with your drink the wait staff will swoop down and ask if you want to place another order (i.e. a hint to pay more or get out).
Compare this to earlier times when it might have been common and socially acceptable to sit for hours on a single purchase and just shoot the shit with fellow townspeople.
there's diners and bars in every corner of middle America. What's changed, I think, is the level of striverism among young people.
In this thread you have multiple people saying they can't go out without paying 200$ or ordering 8$ beers. If you're in your 20s or 30s just go bar hopping in whatever the rundown part of your town is like people used to instead of going fine dining.
A movie ticket, inflation adjusted, costs the same as it used to for decades. Normal people just took it for granted that they had to smuggle some beers into the cinema rather than turning the whole evening into some hundreds of dollars spending spree.
> A movie ticket, inflation adjusted, costs the same as it used to for decades.
Maybe so, but it doesn't feel like that to people. A lot of things are actually way cheaper than they used to be inflation adjusted (we complain about an $80 video game, but inflation adjusted they used to be well over $100, cheaper now even with all the microtransactions, we just remember a sticker that said $50). When I know that a decade ago I could see a $5 matinee and for $20 have drinks and popcorn too, knowing that $40 (albeit for a smaller drink/popcorn) isn't really twice the price doesn't stop the sticker shock, especially for people whose income didn't go up at the same rate as inflation.
NYC is a thriving city of 8.5 million people and one of the most economically active cities in the world, so your experience may be different than say, Gary, Indiana.
Thank you! I skimmed these citations and I remain unconvinced. But I think really answering the question would be a real research project, not a HN back and forth :)
The first citation's relevant highlight is "All categories of third places experienced widespread closures from 2019 to 2021" which is obviously a COVID phenomenon and not a cultural trend. They admit so much. Data from that period I would say is generally irrelevant to discussing wider cultural trends. In fact a query to Gemini says that the number of independent (not chain) coffee shops is growing at 3.2% across the country and it gives this citation: https://www.locationscloud.com/research-report/us-coffee-sho...
The other Science Direct article says "Third places _may_ be closing in neighborhoods across the United States" (my emphasis).
The remaining articles seem to be opinion articles without hard data. They focus on the hypothetical problem of third places going away. In fact the AEI article talks about zoning which cannot possibly be of relevance to any decline in third places given that zoning is becoming less restrictive over time in the last decade.
Part of it may be high rents. I read that rents increased a lot because of fashion stores. They make so much revenue per hour that more traditional stores (like the laundry, the washing machine store, the sewing store, the tabletop games store, and maybe cheaper cafes and restaurants just can't compete.
I have 3 VPSs so that I can run redundant copies of the data scraping software I wrote [0]. I've been scraping NYC subway data for 5+ years.
The biggest VPS hosts my NYC subway times app, my personal website, and other tools I build (most recently my pottery project management tool [1]).
Then in addition I've a bunch of monitoring software. I also run a rollouts system that automatically rolls out new versions of my projects when the GitHub CI builds them.
It's a really interesting thing to do! The maintenance is kind of the point: you get to learn essentially how to build a prod deployment.
I feel this comment is based on a misunderstanding of how Lean works. In Lean you don't need to inspect the proof. There is no "closer inspection". All the human needs to verify is that the statement of the theorem is translated correctly from natural language to Lean. That usually covers a very small surface of the Lean code.
That is an idealized caricature, and far from the reality. One needs to validate the statement of the theorem and the boundary conditions needed to prove it (definitions, axioms, kernel soundness, etc), a la dependency injection. Mathlib is a common shared platform of vetted truths, but not all proofs restrict themselves to Mathlib AFAIK, and neither is Mathlib perfect -- particularly subtle mismatches in the definitions.
> All the human needs to verify is that the statement of the theorem is translated correctly from natural language to Lean. That usually covers a very small surface of the Lean code.
That's exactly what the navier stokes paper posted yesterday pointed out where the LLM bends the Lean code to make it "compile", because the NL might be wrong to begin with or because it missed a detail:
For complex / tedious proofs I can easily see how small details like this can lead to a valid lean proof (or valid "code"), but missing the important details that got lost.
Oh I fully understand how Lean works, how minimal the kernel is etc. I just think that just because "it compiled", we don't actually know that the autoformalization proved all the right stuff along the way. After all, LLMs can produce correct proofs for statements that don't align with the original intended theorem [1]. I just think we should be a bit more skeptical in general before saying these seminal results are fully true. What's the rush?
If it was as simple as that we'd have many more computer-generated proofs than we have now and the Gen AI results would be unremarkable.
Take the Rieman hypothesis. All one would have to do to prove or disprove it would be to encode the statement of the hypothesis in Lean, press enter, and we're off to the races.
That's not how it works. Essentially you have to encode all the intermediary steps of the proof in Lean too, and then Lean can check their correctness for you and check that they lead to each other. But it won't just generate a whole proof from nothing. That is the whole point of the Gen AI math claims.
The person you responded to wasn't saying that Lean magically generates proofs, and all you have to do to create one is feed the problem into Lean. They were saying that, _given a Lean proof_, you can trust Lean to have verified that the steps in the proof are valid, and all you need to do manually is confirm that the theorem was correctly encoded. (IDK if that's true or misses important nuances, but it's not the obviously silly claim you read it as.)
Just to be clear, I'm not trying to willfully misunderstand the OP's comment just to be argumentative. The OP said this:
>> All the human needs to verify is that the statement of the theorem is translated correctly from natural language to Lean. That usually covers a very small surface of the Lean code.
As far as I understand the comment "the statement of the theorem" is the declaration of the theorem to be proved, not its proof. That it "usually covers a very small surface of the Lean code" also implies that the OP was only referring to the theorem, the thing to be proved, and not the proof that can run into many thousands of lines.
If I misunderstood then I don't think that's a problem? I don't believe my comment above comes across as rude or an attack on the OP? I think it's normal for this site for users to correct one another without it being a cause for bad feelings.
I may be misunderstanding you, but I think our point of confusion/disagreement is that you're still reading them as talking about how Lean proofs are created, whereas, given the context, I'm confident they were talking about how Lean proofs are reviewed (after being created by a human or LLM).
I hope there's no hard feelings, by the way -- I wasn't meaning to be nasty to you in that comment. I guess I thought your reading was a bit uncharitable, but I understand that misunderstandings happen (very much including on my end) and I didn't mean to make a big thing of it, so I'm sorry if I came across rudely.
I'm sorry but this is _obviously_ not what I think. I _obviously_ don't think that merely typing a statement into Lean gives us a magic Lean proof. I am even aware that such a SuperLean is not even theoretically possible because of undecidability/halting problem/etc.
A tiny fraction compared to the proof, I'm guessing.
But the point is that you don't need to check the proof. But a lot of people seem to misunderstand what's happening and think you still need to check the Lean proof that AI outputs.
I wonder how Airbnb would respond to a host complaint that uses this data, because of the following story:
A few years ago me and a bunch of friends rented a big Airbnb with a no dogs policy. Some other friends were in the same town, with a dog, and came over and hung out in the yard for a while with their dog. The dog also briefly went in the house (which I think is poor form, to be clear). Somehow the Airbnb host was in the neighborhood and drove by the house to check on it, saw the dog, and then messaged Airbnb to complain.
My friend counter-complained to Airbnb that the host was surveilling us. And the end result was that Airbnb discounted the Airbnb by 50% (over $1000). The owner got nothing out of it. Very surprising to me.
> The dog also briefly went in the house (which I think is poor form, to be clear).
Extremely poor form. Dog people seem to struggle with accepting these kinds of boundaries around their dogs for reasons I’ve never understood.
Although I don’t think the dog should have been in the yard, either. No dogs means no dogs. There can be liability/insurance reasons on top of just not wanting dog shit in your yard.
> My friend counter-complained to Airbnb that the host was surveilling us.
I can’t imagine being an Airbnb host with issues like this.
I’ve stayed in plenty of airbnbs where the owners lived nearby, and noticing a tenant breaking the rules when you drive by doesn’t sound like surveillance.
Basically a similar technical disruption to what's happening in software engineering, but the implications are vastly different because the goals of software and math are not the same. For math, the disruption is leading to a deeper crisis of "what does it mean to be a mathematician?" Whereas for software "what does it mean to be a SWE?" hasn't really changed (the goal is to land software that does things for someone), rather the tooling has changed.
In more detail: in recent years there has been an effort to formalize mathematics using Lean and similar "theorem provers". You write your math proofs in a form of textual source code that Lean can verify for truth. But now Claude Code can produce source code to solve software problems (write me a tool that does X) and also produce source code to solve math (write me a Lean file that proves Y). Historically the main goal of math was to be solve big problems, but now Claude Code can do it. So what does a mathematician do?
Again, I think it's a more dire situation than for software because merely writing the code was never the full job. But for math writing the full proof kind of was.
The argument is a bit more nuanced than this. Historically, the failed paths on the way to proving a theorem led to newer avenues. When this is cognitively offloaded to an llm we are missing out on those developments which the process generated.
This is a great observation. Options induce the worst kind of FOMO. People think: if only I had exercised I would now have $HUGE amount of shares. But the general counter-factual is that you exercise them and sell them pretty soon.
Agreed that this is why a lot of people support the current UB situation, but the history of UB makes this feel wrong:
> As far as I can tell, C89 did not use performance as a justification for any of its undefined behaviors. They were non-portabilities, like signed overflow and null pointer dereferences, or they were outright bugs, like use-after-free. But now experts like Chris Lattner and Hans Boehm point to optimization potential, not portability, as justification for undefined behaviors. I conclude that the rationales really have shifted from the mid-1980s to today: an idea that meant to capture non-portability has been preserved for performance, trumping concerns like correctness and debuggability.
Oh undoubtedly; I didn't mean to imply that performance was the reason behind the origin of UB, though I can see how my comment would read that way. Thank you for adding the note!
Although now for all technical blog posts to HN I feel I should respond: such a weird way of flexing "I have a 6 figure tech job".
reply