I think that the field of proofs, such as LEAN, which have states (the current subgoal), actions (the applicable theorems, especially effective in LEAN due to strong Typing of arguments), a progress measure (simplified subgoals), a final goal state (the proof completes), and a hierarchy in the theorems so there is a "path metric" from simple theorems to complex theorems.

If Karpathy were to focus on automating LEAN proofs it could change mathematics forever.