Formalization of informal ideas will not be the hard part. AI will enable not just automated proofs, not just automated conjectures, but also automated formalization of informal intuitions.
This seems both surprising and extremely crux-y to me. I’m curious if you can offer pointers (beyond “read all of Sahil’s work”) to the best arguments for this.
This seems both surprising and extremely crux-y to me. I’m curious if you can offer pointers (beyond “read all of Sahil’s work”) to the best arguments for this.