alt Hacker NewsWhen math is so divorced from science and engineering that there's no conceivable way that it will ever be applied in the real world then it is just a complex puzzle game that a tiny group of people play. It doesn't really matter much. If the 200,000 line Mathslop proof has no real world application and it doesn't help the puzzle solvers then it is double useless.
Right; this is my viewpoint too. All the "pure mathematicians" have a bleak future where AI can do all the puzzle solving better and faster. They existed in their own world elevating "theorem proving within a formal system" as the central aspect of "proper" mathematics and everything else as ancillary.
It always felt wrong to me that while the scientific method iterated starting with the "real world" viz. Observe, Measure, Hypothesize (includes modeling with mathematics), Test and Refine; pure mathematicians lost themselves in the formalization of hypothesizing/modeling and thus lost touch with mapping it to reality. The AI revolution is now showing them up.