margorczynski

Yeah Youtube has no real competitor and AI shouldn't disrupt it that much, aside from the inflow of AI generated content which might be a problem on the storage cost side.

But most of Google's income is from search and AI/LLMs are killing it off pretty fast. Maybe they'll try to more forcibly inject ads into the summary output.

Probably a mix of both. There's a gigantic amount of costs (and debt) piling up for many companies without anything to show for it when it comes to generating revenue.

But for sure a lot of businesses are getting disrupted - Adobe and now Google are good examples. Just that Google has quite a lot of areas where it shouldn't be so bad - Android, Youtube, mail & storage, cloud. And AI lets them reduce headcounts which is a very big cost.

V4.1-Flash is probably quite smaller and much more resource effective than the frontier models. Add to that much cheaper energy in China.

I would add to that for sure games - a big reason new games, especially AAA, have such a rough time now.

That might have worked if not for the Chinese models. There is no sensible moat to guarantee them (US AI companies) the margins they need to be profitable.

The financial value you can extract from math capabilities is minuscule compared to software engineering.

The problem is you're focused on 1st order effects. I presume you work at some company that sells a product or provides a service - what happens if the demand for that evaporates because the clients can do it themselves or the market has been flooded by much cheaper alternatives created using AI? Or people who bought the product can't do it as they lost their jobs to automation?

This is the same naivete that I saw in coding some time ago before most people finally accepted there is no going back and the times of writing code by hand are gone.

And the guy is not a mathematician primarily - he's a Youtube creator and entrepreneur. I liked a lot of his videos but now I usually just ask the LLM for detailed explanation and I can probe it as much as I want if something is not clear enough.

Education will also take a huge hit, you can't really beat an almost free supergenius that has all the time in the world to explain something to you in as much detail as you wish.

It mostly is. Just that "spiritual" doesn't automatically mean something mythical like God. It can be politics, astrology, social justice, philosophy, etc.

Something that we think is very important to us and the World and bigger than us.

Reads in a lot of places a bit like a mix of anger and bargaining. There is no putting the genie back into the bottle.

But I understand that for people whose whole life was math and solving math problems this will lead to an identity crisis. Seen the same in my area of work (software engineering)

The write-ups are one thing and more of a cherry on top but I would say the more pressing matter is the lack of Lean formalization which means you can't really say it has been (dis)proven or not.

If you do a dump like this all of it should be formalized, there's simply too much material to review by hand and additionally it is AI-written which makes it hard to read compared to human work.

How does the price compare to Luna? At least looking at the numbers it is noticeably better at most tasks.

Verify the statement is correct + it doesn't introduce any new axioms + doesn't use "sorry" etc.

Order of magnitudes easier than verifying the whole thing by hand and gives a much better guarantee of correctness

> reviewing proofs it creates?

If you mean reviewing for correctness then no, a Lean proof is a much stronger guarantee than anything that can be provided by any human.

For someone who's goal in math was taking unsolved problems and working on them then it's probably over. Just like in software engineering writing code by hand is kinda over.