David Hilbert famously said "We must know. We shall know." AI is making it all too easy to focus with excitement on the "know," and we are at risk of forgetting the "We." If there was ever a time to remember -- not only in mathematics, but in every field -- that human society exists for humans, and efficiency is only good if it is good for humans -- this is certainly it.
This might be a dumb thing to say, but doesn’t AI create interesting work for mathematicians? Disproving plausible but flawed arguments, proving that a paper relies on unattributed material - isn’t that the fun stuff?
AI is unlikely to create anything interesting for me, but many of the authors of the Declaration are quite keen on AI. Nothing you wrote is inconsistent with the purpose of the Declaration, which is to "protect the core values of mathematics."
I don't see that this declaration takes into account that the possibility to formally check mathematics is transformative in combination with AI. It's basically obsolete already today.
That actually sounds harsher than I intended it to sound. What I mean is that formal verification is not just "one more thing" that this declaration needs to take into account. Rather, it should be central to it, and its consequences. For example, it *should* transform peer review in that a blog post (or a paper posted on the arxiv or zenodo) is enough, if it comes with enough evidence. So we should be discussing what exactly evidence looks like, not where it is published. This avoids the common gate keeping seen today, where personal opinions and agendas of reviewers usually trump objectivity.
Different authors of the Declaration had different opinions on this particular question. I certainly don't think the word "transformative" is at all appropriate. Reasons for my belief have been shared frequently in this newsletter, and I'll probably return to it again in the future.
Let me also say that I think that formalisation, and the search for the right way to formalise mathematics, is a deeply mathematical endeavour. Mathematicians should not be standing at the side and let computer scientists run with their type theories (which is definitely not the right way) all over them. Embrace formalisation and make it yours, because that is where it belongs.
I amended my comment with the second paragraph before seeing your reply, but I guess it does not change much in that respect. Is it transformative, or not? This question has a clear answer, and time will tell what it is.
Thank you for this.
David Hilbert famously said "We must know. We shall know." AI is making it all too easy to focus with excitement on the "know," and we are at risk of forgetting the "We." If there was ever a time to remember -- not only in mathematics, but in every field -- that human society exists for humans, and efficiency is only good if it is good for humans -- this is certainly it.
I appreciate this thoughtful statement.
Seems to me this entire argument could be resolved with three words: “Show your work”.
This might be a dumb thing to say, but doesn’t AI create interesting work for mathematicians? Disproving plausible but flawed arguments, proving that a paper relies on unattributed material - isn’t that the fun stuff?
AI is unlikely to create anything interesting for me, but many of the authors of the Declaration are quite keen on AI. Nothing you wrote is inconsistent with the purpose of the Declaration, which is to "protect the core values of mathematics."
I don't see that this declaration takes into account that the possibility to formally check mathematics is transformative in combination with AI. It's basically obsolete already today.
That actually sounds harsher than I intended it to sound. What I mean is that formal verification is not just "one more thing" that this declaration needs to take into account. Rather, it should be central to it, and its consequences. For example, it *should* transform peer review in that a blog post (or a paper posted on the arxiv or zenodo) is enough, if it comes with enough evidence. So we should be discussing what exactly evidence looks like, not where it is published. This avoids the common gate keeping seen today, where personal opinions and agendas of reviewers usually trump objectivity.
Different authors of the Declaration had different opinions on this particular question. I certainly don't think the word "transformative" is at all appropriate. Reasons for my belief have been shared frequently in this newsletter, and I'll probably return to it again in the future.
Let me also say that I think that formalisation, and the search for the right way to formalise mathematics, is a deeply mathematical endeavour. Mathematicians should not be standing at the side and let computer scientists run with their type theories (which is definitely not the right way) all over them. Embrace formalisation and make it yours, because that is where it belongs.
I amended my comment with the second paragraph before seeing your reply, but I guess it does not change much in that respect. Is it transformative, or not? This question has a clear answer, and time will tell what it is.