# Notes on a Path to AI Assistance in Mathematical Reasoning

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

## Key facts

- No citing papers in the map yet (data through 14 Oct 2026).
- Builds on 6 of its 20 references that are in the map.
- First posted on arXiv 4 Oct 2023.

## Builds on (most cited first, 6 of 6)

- [Draft, Sketch, and Prove: Guiding Formal Theorem Provers with Informal Proofs](https://mlsanity.com/paper/2210.12283/) (2022)
- [Autoformalization with Large Language Models](https://mlsanity.com/paper/2205.12615/) (2022)
- [HyperTree Proof Search for Neural Theorem Proving](https://mlsanity.com/paper/2205.11491/) (2022)
- [Murmurations of elliptic curves](https://mlsanity.com/paper/2204.10140/) (2022)
- [Formalising perfectoid spaces](https://mlsanity.com/paper/1910.12320/) (2019)
- [Formalizing the Solution to the Cap Set Problem](https://mlsanity.com/paper/1907.01449/) (2019)

## Abstract (arXiv)

These informal notes are based on the author's lecture at the National Academies of Science, Engineering, and Mathematics workshop on "AI to Assist Mathematical Reasoning" in June 2023. The goal is to think through a path by which we might arrive at AI that is useful for the research mathematician.