Immediately after the launch of GPT-4, I tried to use to write proofs in an unpublished formal systems I’ve been working on. The results were quite astonishing. You can find the paper, “Experimental results from applying GPT-4 to an unpublished formal language“, on arXiv: https://arxiv.org/abs/2305.12196

Abstract. 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.