[mathgradthrow]

The terrifying thing about lean and machine learning is not the idea that we will train computers on human written proof, but that we won't have to. With the rules of chess easily computed, a computer can use the bellman equations and self play to learn a policy that is vastly superior to human play, at least on the critical path.

The state space of mathematics is pretty different from chess, but I think ultimately, mathematicians are just running something like A* on the space of propositions, with a custom heuristic that is learned by approximating the result of running A* with that heuristic. where your error is just the difference between the actual and predicted length of proof.