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.
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.
Maybe tiring, but that is the reality. Note that mathematicians are only upset now that "have you tried this on the latest model" works for so many of their problems now, but didn't for the model before that.
Those are the two extremes, both are just as bad. Don't excuse shortcomings of the current models with promises of future improvements. But also don't demand literal miracles in 21 business days.
unddoch · · focus · HN ↗
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 · · focus · HN ↗
amoss · · focus · HN ↗
auggierose · · focus · HN ↗
Xirdus · · focus · HN ↗