4 ms·
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 s
by daly 2y ago
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.
- jomohke 2y agoDeepmind'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-at-silver-medal-level/ https://deepmind.google/discover/blog/ai-solves-imo-problems...