I will be starting a CS PhD in formal methods (mathematucal formalizations and proofs for programs and languages) in October. By when will AI be executing most of my research, with me reviewing and setting goals?

Writing code and formal proofs (e.g. lean, which I'm probably going to be doing the formalization in) is not sufficient to resolve YES. A YES resoution requires e.g. AI taking over most low and medium level design decisions, autonomously proposing, reseaching, comparing, and evaluating on different design approaches competently enough that I am satisfied with the reasoning presented to me and do not feel like I have to step in to fix bad decisions and missed opportunities.

In my current reeearch so far, I have not really seen this with claude at all. I think it's mostly because good high level decisions require keeping a wide context of self deveolped solid concepts in view, and somehow LLMs seem to tend to keep everything they come up with very liquid and subject to reinterpretation.

Resolves when I look back on the last month, and decide that I think AI has been executing most of my research in the last month.

I'll update this market with how things ate going if I feel like there has been notable progress in this direction.

I will not bet in this market.