Other tribe not hate whispering rock. Tribe hate rock salesman saying it solve every problem. Thinking rock make many wrong marks! Shaman must check every mark himself! Whispering rock speak with big confidence even when wrong. Dangerous rock! Who clean mess? Shaman! Soon shaman forget how to hunt! Today rock help shaman. Tomorrow chief say no need shaman. Me worry.
So do humans. Don't Lean proofs take care of that?
https://terrytao.wordpress.com/2024/12/05/ai-for-math-fund/
He is leading another AI foundation:
He is partnering with the commercial startup math.inc (funny name, isn't it?):
https://www.math.inc/a-conversation-with-terry-tao
He is knee deep in the AI money. This submission is him desperately trying to simplify a spaghetti AI proof (i.e., menial work) to show that AI works. He didn't discover anything new.
Tao: “There will be some places where we should use AI, but we should take initiative and decide what those are,” he said. “We set the rules on what’s acceptable or not, and we should not let external actors define those for us.”
https://www.simonsfoundation.org/2026/08/13/fields-medalist-...
isn't the linked post precisely an example of the opposite?