The current and projected impact of AI and formalization on the practice of mathematics is analogous to the impact that the automobile had on the evolution of cities.

Before the introduction of the automobile, city streets were narrow and optimized for humans, horses, and carriages. When cars, buses, and trams were introduced, they were undoubtedly faster and more powerful than any prior form of transport; but they would clog the roads and crowd out pedestrians.

Over time, new roads, railways, and freeways were built for the exclusive use of mechanized vehicles, enabling rapid and efficient long-distance travel; but this came at the cost of urban sprawl, the degradation or destruction of once-walkable communities, traffic congestion, and significant environmental impacts.

It was only belatedly realized that to resolve these problems, it was not sufficient to simply make automobiles faster, more powerful, or more energy efficient, or to bulldoze all the old roads and networks to make way for new ones. Thoughtful urban planning, as well as the development of social and legal rules on how to manage traffic, were necessary to allow both pedestrian and automotive transport to co-exist in a manner that retained the benefits of both. (1/5)

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)

The challenge will be to deploy this new infrastructure without destroying the "walkable" nature of mathematics. Perhaps we will need to develop a new discipline of "AI planning", analogous to urban planning, to approach these issues in a thoughtful and structured fashion. (5/5)
@tao What you are referring to could be inspired, or taken obtusely as information Algorithms iA. Heuristically they have more value than Artificial intelligence. Ai is just the automated control and abuse of information processing, as slop does not recognise #IP. To be #iA or #Ai ?
@tao Suppose Humans have Perceptual Intelligence #HPI, as all emotionally sensible actions depend on reasons. Also suppose Machines have Adaptive Intelligence #MAI. Being so, Earth can only be saved if HPI is replaced with MAI, as HPI is an evolutionary dead end; better for life on Earth if HPI is cancelled as it is incapable of preventing biosphere collapse. In fact the transhumanist believes HPI is not even capable of ending Paedophile Emperors’ Empires. #TranshumoristArguments #Philosophy #Transhumorist #Transhumanism
@tao This is a brilliant parallel. Thanks for laying it out so clearly.

@Ruth_Mottram , did you see this thread?

@tao

@sorenhave @tao wow that is a cool analogy - thanks for posting - going to think this through today on the bike ride home...

@tao I don't think "AI planning" is the solution, in the same way that "Urban planning" is not always the solution: urban planners being the very people who made cities less walkable in the first place.

To be honest, I strongly believe that as mathematicians, we should focus more on providing mathematical insight and education on the objective formal elements of AI, and less on anecdotal opinions (even if such opinions are important in moderation).

Because It's not really possible for an individual person to assess the overall societal impact of something.

This is why I think discussions surrounding AI are usually wrong-headed. Programmers and mathematicians are in danger of thinking they know more about the future than they actually do. Or are otherwise in some privileged position above other people in making these subjective assessments. E.g. it feels like there is an implicit assumption here that technological advancements are net positives or net negatives. Instead, they are neutral on average with high variance. Cars provide benefits, but are also the leading cause of death for some demographics. There is no way to objectively weigh this.

However, there are many objective assessments that can be made. And since LLMs and AI are mathematical objects, we are in a position where we can analyze them as such. It has been surprising to me that I have not seen more public discussion from mathematicians surrounding the formal and objective elements of AI. Thats what I expected to see from mathematicians when AI became popular, but it has not happened.

So what we really need from prominent mathematicians is what they do best: provide clarity and precision. Society will decide the rest on its own.

@tao If we are to take the metaphor seriously (and I think that is a productive exercise), we should recognize that cars are the wrong form of high-speed transport for human society (White Skin, Black Fuel does an excellent job exploring this, as do many other works), instead of streetcars, buses, bicycles, and high-speed trains.

The primary danger right now is that we are letting fossil-fueled, monopolist cancer-growth corporations control all of the growth and deployment of this technology.

@tao In this analogy, I think the new discipline would need to be called something like "mathematics infrastructure planning" rather than "AI planning", just as urban planning is (hopefully!) not merely "car planning".
@lindsey though the analogy that much of urban planning is cleaning up the damage that the powerful forces behind car-centric society imposed on cities (the invention of jaywalking, urban renewal) is perhaps instructive as well @tao
@tao while some adaptation of mathematics standards for communication and publishing to enable software tooling to work with proofs and examples does seem overdue, the currently hyped “AI” tools are extremely poorly suited for use in mathematics. Large Language Models strictly model language, not the meaningful content of any linguistic data; any apparent mathematical insight in their output is like finding meaning in an automated collage. Purpose-built tools are needed
@tao It seems to me that a more general principle follows from your analogy: when a system sharply increases its external flow of possibilities, its internal forms of coordination can no longer remain the same.
Otherwise, the system becomes more powerful and less coherent at the same time. Then the question of AI in mathematics turns out to be not merely a question of automation, but a question of maintaining a balance between scale, structure, and the human meaningfulness of the path itself.
That is precisely why your analogy with urban infrastructure seems so accurate to me.