Post #4060072

Yesterday a really good mathematician told me Anthropic is paying experts like him $250/hour to improve Fable by throwing hard math problems at it. They also get a separate account where they can use Fable for their own purposes. They can do this for 5 months maximum. On Bluesky someone asked me if I'm interested in this sort of thing. An ambiguous question. I said I'm not interested in working for an AI company, but I'm *extremely* interested in the battle for the soul of mathematics that is heating up. On the one hand, some of these LLMs are getting very good at solving math problems - when used by someone who knows what they're doing. The person I spoke to was in awe. He could ask it hard questions about generalized cohomology theories and it could compute the answers using clever tricks without being told which tricks to use. On the other hand, Kevin Buzzard, who is always pushing for the computer formalization of mathematics in Lean, says any PhD student who is not paying $200 per month for an AI subscription is "crazy". Does he really think they're all so rich? Is this what we want being a mathematician to become: paying a lot of money for an AI subscription to help you prove theorems and formalize them in Lean? So dull. https://xenaproject.wordpress.com/2026/07/20/human-mathematicians-are-being-outcounterexampled/