returningfory2

He has over quarter of a million subscribers so presumably it's his full time job?

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".

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.

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.

Right. Has that changed? Asking genuinely.

> 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?

> Does it count as a third space if you have to pay for it?

Yes, third spaces/places include places you need to pay for.

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.

Sorry to be a bit snarky, but I feel like the comment was kind of equivalent to calling me an idiot.

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 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.

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.

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.