For every important match problem solved by AI, without mathematicians we wouldn't know about the existence and importance of the problem.

Famous mathematical conjectures are social constructs, formed by decades of even centuries of attention given to them by members of the math community. Without it, the danger is that future math "progress" will be reduced to generating tables of Lean statements and a probable/unprovable bit generated by AI.

▲

Xirdus an hour ago | parent [-]

Could just be a sampling bias. Humanity had something like 3000 years to make famous conjectures, whereas AI mathematicians have been around for a month or so. Give them time, I'm sure they'll start formulating highly consequential unsolved problems soon enough.

	▲	eru 35 minutes ago \| parent \| next [-]
		Not just sampling bias, but also human bias. In a sense, how do you know whether the problem your AI has just solved is important? A simple proxy is to just check whether humans have thought it's important. That's also why famous open problems are a good benchmark or proxy: you don't need to convince the rest of the world that the problem your lab's new AI just solved is actually useful or hard.
	▲	amoss 37 minutes ago \| parent \| prev \| next [-]
		Somewhat tiring that as alway any criticism is reduced to "but have you tried this on the latest model".
	▲	xanderlewis 34 minutes ago \| parent \| prev [-]
		> AI mathematicians have been around for a month or so. LLMs have been around for years, and they're explicitly trained on the entire history of human mathematics (without which they'd be unable to do anything).