>and don't dream big enough

People have been dreaming running PS5 games on PC for a long time. Just when AI starting to become capable of doing that, Anthropic shut it down.

Yeah you can dream, but only what we allow.

To a first approximation I agree that it’s similar to industrialization. However there’s a key factor which distinguishes this case, and which makes the analogy less than perfect: there isn’t a profit motive in mathematics, so there was no push for this development from inside the field. Instead, the industrialization was entirely exogenous, from companies which do in fact have that profit motive and view math as a means to achieve it.

There might be a “proof motive” in math which one could argue will drive the full automation of theorem proving. But we must recognize that profit is more universally valuable (i.e. it has value outside the industry in which it was created), whereas proofs are only valuable inside the math community (at least the pure math proofs the labs have been publishing thus far).

> It's like seeing a car engine for the first time, lamenting about the future of horses, and not realizing it'll also help us fly.

Only this time we are the horses and argue about the car engine not having the intuition on where to put the hooves.

This is really well put, I totally agree with you.

There’s an immediate resistance towards change rather than embracing it and finding opportunities to improve and work with it.

That is a great example, car engines (and derivatives) did create tremendous economical value but are in the process of making our planet unhabitable.

Maybe we should listen to people that care about negative externalities more often, and actually mitigate them.

> My recent take on AI is that people haven't adapted to the new huge potential of the tool, and don't dream big enough (yet).

I guess you can dream big enough only if you have access to the really interesting models. The 20$ subscription won't get you there, and the 100$ one is already out of reach for so many people.

Two possible walls for advancing math with AI: first, it could be that the kind of problems that AI solves are the ones that don't open new avenues to concepts and ideas, and second, problems complexity is usually not linear, and the new and interesting problems to solve could be at a level of complexity beyond what AI can currently solve. Perhaps mathematicians could work to find ways to help AI cope with those walls.

How you get somewhere is important and tools change how you get there.

You can drive 1000 miles and arrive at the destination on the highway quickly.

Or you can take the slow road and walk. You discover unrelated things, make new relationships, see the scenery, listen and smell what is around you and have time to contemplate things which may or not be related.

This particular tool economy robs us of all these things in the rush to the destination.

I'd sacrifice "progress" a little for some of the better bits of humanity.

Yes, this. Unless there is a true singularity where no more questions are ever asked, there will be definition be infinitely many problems to solve, and most of them we have not even glimpsed yet.

Singularity? Probably not.

Tech bro dictatorship? Unfortunately a bit more likely.

None of the above? Then we have a small shot at a great future.

Having a machine that solves hard problems must be a good thing.