RECORD
Notes on a Path to AI Assistance in Mathematical Reasoning
History and Overview · Submitted 4 Oct 2023
abstract compiled · 2026-09-23 · no language-model review
The authors' main claim The goal is to think through a path by which we might arrive at AI that is useful for the research mathematician.
The compiled record
The paper's own sentences, arranged. Each label is drawn from a closed vocabulary; the number beside it is the probability the classifier gave that label. Numbers in the tables are the authors', checked by code. No sentence in this record was written by a model.
Open the compiled record
The abstract, sentence by sentence
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.
background contribution method result interpretation main claim
| # | sentence | role | the authors' own work | states the main conclusion | strength |
|---|---|---|---|---|---|
| s0 | 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. | background 0.97 | 0.64 | 0.02 | asserted 0.99 |
| s1 | The goal is to think through a path by which we might arrive at AI that is useful for the research mathematician. | contribution 0.49 | 0.17 | 0.11 | speculative 0.66 |
What was examined, and what was not
- arXiv listing abstract v1
- full text
- figures and tables
- references and citing sentences
- relations to other papers
- P abstract
- S sections
- T body sentences
- C citations
- R cross-paper relations
The paper
Original abstract
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.
Human review
How the literature uses it
What this paper does with the arXiv papers it cites
What it cites · 5 sentences without a confident label
Cites as support 2 papers
-
Three vignettes to illustrate this are: * It took two years from Ellenberg-Gijswijt's 2017 solution [ref] of the Cap Set Conjecture to its 2019 formalization [ref] . * It took one year from Gardam's 2021 counterexample [ref] to Kaplansky's unit conjecture for group rings to its 2022 formalization [ref] . * The formalization [ref] of Bloom's solution [ref] to the Edros-Graham density conjecture on Egyptian unit fractions arrived before its referee reports!
On a density conjecture about unit fractions · Paths to Large Datasets of Formalized Mathematics · 0.96
-
AI has also already proved somewhat effective here; see, e.g., [ref] , and the more recent discovery [ref] of murmurations in the Fourier coefficients of elliptic curves.
Murmurations of elliptic curves · Finding a Holy Grail · 0.98
Discussion
Know something about this paper? Leave a comment, or highlight any passage above to comment on it.