You can have your opinions about modern math, its usefulness in the world as it is, whether or not knowing if hairy balls can divide by three is actually going to be beneficial for anything but just obscure knowledge's sake. You may even say it's useless.

Needless to say, a useless result that absolutely no mathematician will ever read, confirm, understand, agree with or even consider to solve their "useless" problems is an impressive waste of resources.

Worthless is a pretty good description IMO in the context of what Lean is trying to achieve: "enable correct, maintainable, and formally verified code". Tens of millions of lines of LLM vomit may be many things, but it often turns out to not be correct and certainly not maintainable. Formally verified remains as a thin fig leaf covering the uncomfortable truth that formal methods only provide assurances under assumptions (your toolchain, libraries, compiler, OS, and hardware are "correct" and don't expose some exploitable flaw).

It doesn't mean that it cannot improve over time, maybe the proof can be "minified" to a state where human reviewers are able to comprehend it; but as it stands there isn't really much insight or confidence to be gained from the artifact itself.

There's a branch of mathematics called "pointless topology" [1].

[1] https://en.wikipedia.org/wiki/Pointless_topology