Broadly, as you'll see in the Google doc linked from the announcement, they are referring to the use of computer systems to assist mathematical research, which falls into a two step process: 1) Identify a suitable language for use by both humans and computers for communication and manipulation of mathematical theorems and their proofs. 2) Employ both mathematicians and machine learning algorithms to generate interesting sentences in that language.
> as you'll see in the Google doc linked from the announcement, they are referring to the use of computer systems to assist mathematical research, which falls into a two step process
I reviewed the doc, and it is just curated list of links on various projects (ML frameworks, proof assistant, some tutorials), and does not outline plan you described here. Or I missed something?..
The first section, Textbooks and Survey Papers, begins with Formal Proof (this is where one identifies the suitable language for mathematics), followed by general Machine Learning references, and concluding with Machine Learning for Formal Proof. Other sections have similar divisions, though some go off into adjacent fields where one finds non-AI* algorithms for specific mathematical applications, such as automated symbolic calculus or SMT solving, to name just two.
*Some people's terminology would classify such algorithms as "AI". I wouldn't, but they are nonetheless on-topic because you might invoke them to assist, focus, refine, or accelerate other techniques.
