OpenAI has managed to derive a number of Metamath proofs, some of which are smaller than the human-created proofs, using machine learning. Here is a gource vis

OpenAI has managed to derive a number of Metamath proofs, some of which are smaller than the human-created proofs, using machine learning. Here is a gource visualization of metamath proofs overtime in the set.mm database: https://m.youtube.com/watch?v=LVGSeDjWzUo https://m.youtube.com/watch?v=LVGSeDjWzUo Note that near the end, one of the contributors is OpenAI, who is not a human contributor.