On: Why do we need human mathematicians anymore?

[red75prime]

Brute-force search is called that specifically for its lack of sophistication. A "sophisticated brute search" is an oxymoron.

[vatsachak → red75prime]

You're right. But...

Spending 132 billion tokens is definitely way more energy than human mathematicians would have thrown at the problem and probably would have solved within two years.