Computers do nothing but process logical statements. Mathematics consists of nothing but such statements. It would be reasonable to assume, then, that computers would be adept, perhaps uniquely, at reading, understanding, and cataloging the academic literature of mathematics. Not yet. People and machines, it turns out, speak different mathematical languages. If computers are to help manage mathematical knowledge, they need to be taught how to read math papers. The grant funds efforts by mathematician Thomas Hales to begin that instruction. Hales has raised an international army of graduate students and postdoctoral researchers, which he plans to unleash on the abstracts of thousands of mathematical papers. They will carefully translate the definitions and results that appear in these abstracts into formal programming language. These formalized abstracts—“fabstracts,” for short—can then be used to train machine learning algorithms to “read” textual mathematics.