# Experimental results from applying GPT-4 to an unpublished formal language

arXiv: https://arxiv.org/abs/2305.12196 · HTML: https://mlsanity.com/paper/2305.12196/

## Key facts

- Cited by 3 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 20 May 2023.

## Built on by (most cited first, 3 of 3)

- [Grammar Prompting for Domain-Specific Language Generation with Large Language Models](https://mlsanity.com/paper/2305.19234/) (2023)
- [A Survey on Deep Learning for Theorem Proving](https://mlsanity.com/paper/2404.09939/) (2024)
- [Grammars of Formal Uncertainty: When to Trust LLMs in Automated Reasoning Tasks](https://mlsanity.com/paper/2505.20047/) (2025)

## Abstract (arXiv)

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.