[kvemkon]

> What we need is automated theorem discovery.

I've been thinking mathematicians have fun doing math, making discoveries, crafting proofs.

Does Tour de France & Co. make no sense since small, lightweight and powerful e-bicycles appeared?

Using computer as a helper like bicycles is one thing, using LLMs seems more like e-bicycle and is something another.