EvoGPT-f: An Evolutionary GPT Framework for Benchmarking Formal Math
  Languages
Johnathan Mercer
Formal mathematics is the discipline of translating mathematics into a
programming language in which any statement can be unequivocally checked by a
computer. Mathematicians and computer scientists have spent decades of
painstaking formalization efforts developing languages such as Coq, HOL, and
Lean. Machine learning research has converged on these formal math corpora and
given rise to an assortment of methodologies to aid in interactive and
automated theorem proving. However, these papers have primarily focused on one
method, for one proof task, in one language. This paper introduces EvoGPT-f: a
novel evolutionary framework for the first systematic quantitative analysis of
the differential machine learnability of five formal math corpora (Lean 3, Lean
4, Coq, HOL 4, HOL Light) using four tokenization methods (character,
word-level, Byte Pair Encoding and StarCoder tokenizer). This paper does not
put to rest the question of the "best" or "easiest" language to learn. Rather,
this framework and preliminary findings begin to illuminate the differential
machine learnability of these languages, offering a foundation to forge more
systematic quantitative and qualitative comparative research across
communities.