He sees value in mathematicians using AI to carefully study mathematics, develop an understanding of both old and new things, and help others understand the new things.

He doesn't see value in scrolling through unsolved problems asking an AI to please solve them. In his view, this is a fundamental confusion about what mathematical research is for. Knocking down unsolved problems without developing the community's understanding of them is like prompting Claude to go through a Jira board, write code for all the open tickets, and then close them without merging or deploying the code.

▲ bluecheese452 2 hours ago | parent [-]

Isn’t it more like it merges the code without a dev reviewing or understanding it?

	▲	dbmikus 2 hours ago \| parent \| next [-]
		Pretty close, but IMO not quite. A math proof in and of itself is useless unless either: `(A) it furthers human knowledge (B) it gets used in applied sciences, engineering, etc.` If you merge and deploy code, you have released a tool that can be used. If you ship a gibberish math proof, it's not useful unless someone else can understand and deploy it to some other means. Now, it's possible AI could understand and make use of the math proofs, even if we can't, which refutes some of my hair splitting :)
	▲	SpicyLemonZest 2 hours ago \| parent \| prev [-]
		No. Merged code can perform actions with effects on the world, even if a human being never saw it. Constructing a giant Lean formalization that nobody understands simply doesn't do anything.