​​GPT-f — это языковая модель, которую обучили генерировать доказательства теорем. В качестве архитектуры использовали transformer-модель GPT-3. GPT-f призван ассистировать математикам при доказательстве теорем. Модель работает для формального языка для доказательства теорем Metamath. По результатам экспериментов, GPT-f находила новые короткие доказательства, которые приняли в библиотеку Metamath.