I think it shows that much of coding is a lot easier than we think. Even very challenging programming problems involve a lot of just boilerplate and rote implementation of learned patterns.

Arcane is not the same as actually intellectually hard. Programming is arcane.

Same with circuit layout, which is also amenable to things like genetic algorithms, and yes I believe math proofs might be easier than we thought.

It seems to be that you can mix some intelligence and a learned bag of motifs with iterative gradient descent and solve math proofs like a hard jagged optimization problem. I feel like this is what has been demonstrated. You get a huge blob of Lean but it works.

We might learn there are domains like, say, nursing or writing (good writing) or blue collar work or being a secretary for a large company that require a lot more fluid intelligence than fields that have historically been smug about their high IQ requirements.