Bibliography (5):

1. A general reinforcement learning algorithm that masters chess, shogi, and Go through self-play

2. Generative Language Modeling for Automated Theorem Proving

3. MiniF2F: a cross-system benchmark for formal Olympiad-level mathematics

4. Wikipedia Bibliography:

   1. Metamath

   2. Lean (proof assistant)