On the usefulness of proving theorems vs. writing them down: I think there’s more of a back and forth. See for instance Nature’s post on how DM used an AI to guide intuition (https://www.nature.com/articles/s41586-021-04086-x).
To me, it’s going to help humans “babble” more in math by using some extension, like a Github Copilot but for math. And I feel that overall increasing math generation is more “positive for alignment in EV” than generating code, especially when considering agent foundations.
Besides. in ML the correct proofs can happen many years after algorithms are used by everyone in the community (e.g. Adam’s proof shown to be wrong in 2018). Having a way to have a more grounded understanding of things could help both for interpretability & having guarantees of safety.
On the usefulness of proving theorems vs. writing them down: I think there’s more of a back and forth. See for instance Nature’s post on how DM used an AI to guide intuition (https://www.nature.com/articles/s41586-021-04086-x).
To me, it’s going to help humans “babble” more in math by using some extension, like a Github Copilot but for math. And I feel that overall increasing math generation is more “positive for alignment in EV” than generating code, especially when considering agent foundations.
Besides. in ML the correct proofs can happen many years after algorithms are used by everyone in the community (e.g. Adam’s proof shown to be wrong in 2018). Having a way to have a more grounded understanding of things could help both for interpretability & having guarantees of safety.