Experimental results from applying GPT-4 to an unpublished formal
  language
Gregor vom Scheidt
Can large language models be used to complete mathematical tasks that are
traditionally performed either manually or with the aid of theorem provers? To
answer this question, a state-of-the-art system, GPT-4, was provided with a
concise natural language specification for a previously unpublished formal
system and asked to complete a number of tasks, from stating function and type
definitions to proving simple theorems and verifying user-supplied proofs. The
system completed all tasks successfully, showed extensive domain knowledge,
invented helpful new syntax and semantics, and exhibited generalization and
inference abilities. So the answer seems to be: yes.