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.
Deepmind's recent model is trained with Lean. It scored a silver olympiad medal (and only one point away from gold).
> AlphaProof is a system that trains itself to prove mathematical statements in the formal language Lean. It couples a pre-trained language model with the AlphaZero reinforcement learning algorithm, which previously taught itself how to master the games of chess, shogi and Go
https://deepmind.google/discover/blog/ai-solves-imo-problems...