> He doesn't see value in scrolling through unsolved problems asking an AI to please solve them.
replyYet that's exactly how the field works. A new grad student is tasked with finding a suitably difficult problem from a list of unsolved problems. The sweet spot is obscure, so that fewer people are working on it, but not too obscure that no one knows about it. It works the same way in theoretical physics and theoretical Comp Sci, and I speak from insider knowledge. The rosy view of mathematicians in the media is largely a product of marketing.
The authors of the declaration agree with you that this is how the field works today. They think that fact causes AI use to produce bad results, and they want to reformulate how the field works so that AI use will produce good results instead.
replyIsn’t it more like it merges the code without a dev reviewing or understanding it?
replyPretty close, but IMO not quite. A math proof in and of itself is useless unless either:
reply (A) it furthers human knowledge
(B) it gets used in applied sciences, engineering, etc.
Not necessarily. That's the best case scenario, but proofs can be intrinsically useful in and of themselves. It's just that for problems of that nature, speculative work is often done ahead of time, e.g. the body of work that already exists assuming the Riemann hypothesis is true.
replyNo. 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.
reply