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.
Author here. We were heavily inspired by multiple things, including Demski and Garrabrant, the 1990′s work of Kalai and Lehrer, empirical work in our group inspired by neuroscience pointing towards systems that predict their own actions, and the earlier work on reflective oracles by Leike . We were not aware of @Cole Wyeth et al.’s excellent 2025 paper which puts the reflective oracle work on firmer theoretical footing, as our work was (largely but not entirely) done before this paper appeared.