31 citations · 114 across the 16 of their papers we have counts for
3 papers · 2 filters
Exploration of Neural Machine Translation in Autoformalization of Mathematics in Mizar
Qingxiang Wang, Chad Brown, Cezary Kaliszyk +1
In this paper we share several experiments trying to automatically translate informal mathematics into formal mathematics. In our context informal mathematics refers to human-writt…
Towards Finding Longer Proofs
Zsolt Zombori, Adrián Csiszárik, Henryk Michalewski +2
We present a reinforcement learning (RL) based guidance system for automated theorem proving geared towards Finding Longer Proofs (FLoP). Unlike most learning based approaches, we…
GRUNGE: A Grand Unified ATP Challenge
Chad E. Brown, Thibault Gauthier, Cezary Kaliszyk +2
This paper describes a large set of related theorem proving problems obtained by translating theorems from the HOL4 standard library into multiple logical formalisms. The formalism…