In this analogy, the narrow pre-automotive roads are the social infrastructure of mathematics: papers, journals, conferences, citations, advisor-student or mentor-mentee relationships, job postings, and the like. They are primarily designed for use by humans alone, or humans using only moderate amounts of computer assistance. The analogue of transportation here would be that of proving new results that take one from a given hypothesis to a desired conclusion.

Human mathematicians can generate such proofs, but the process is lengthy and inefficient, usually requiring one to draw upon previous work or collaboration with colleagues or students. But this laborious process also generates many beneficial secondary effects beyond the ostensible goal of getting from hypothesis to conclusion. The author(s) develop skills and expertise for future research projects. Maps of the mathematical terrain can be drawn for subsequent researchers to benefit from, for instance pointing out future directions of research or serendipitious discoveries that the author encountered or glimpsed during his or her journey. Interesting stories - such as encountering a dead end in one's mathematical exploration, and changing course to avoid it - can be told. (2/5)

More automated approaches to proof generation may accomplish the primary goal of getting from A to B much more efficiently, but at the expense of secondary goals, particularly if applied via large-scale, non-interactive workflows, much as how the driver or passengers of a vehicle may arrive at their destination without noticing any interesting features of the intervening terrain. Among other things, this often makes such proofs unsuitable for publication in traditional journals, as the expected narrative that describes the path towards such proof in the context of prior work, and lessons learnt or future directions suggested from the proof process, can be almost completely absent in AI-generated proofs.

One could perhaps try to "upgrade" AI capabilities further to add on these sorts of features to AI-generated mathematics, in order to create AI-generated articles suitable for publication in traditional journals, but to me this is analogous to trying to modify cars to fit into streets designed for humans. In a similar vein, getting AI models to achieve superficially similar feats to recognized human demonstrations of achievement may simultaneously become increasingly impressive and increasingly meaningless, analogous to demonstrating that a car can "win" a marathon by traversing the course in a much shorter time than any human runner. (3/5)

To me, a better way forward would be to develop new machine-friendly mathematical infrastructure, analogous to modern roads, railways, or freeways, that would complement, rather than replace, existing human-oriented pathways and buildings, that can more fully exploit the gains in efficiency and scale that these new technologies can offer.

Large-scale mathematical challenges could be one such example of new infrastructure - somewhat analogous to a high capacity freight corridor - in which an expertly curated set of mathematically interesting tasks or problems are laid out for various participants to solve by whatever means (or level of AI assistance) desired, with solutions being verified by some efficient and trustable process (such as via formal proof assistants) in order to be able to safely handle the high volume that such a challenge would engender.

Or one could use automated methods to develop a large-scale library of low-quality proofs of many existing results in the literature, to be used as a starting point for humans (perhaps aided by specialized AI tools) to create higher-quality proofs that have additional desirable pedagogical, stylistic, or aesthetic features. To continue the transport analogy, this would be like driving along some highway system to a non-descript parking lot in a national park in order to then hike a few additional miles to a scenic destination. (4/5)