Here's an interesting idea. As proofs of theorems become more and more abundant, and as inventing new maths becomes something anyone can do, a new bottleneck is emerging in applied maths.

AI can reason about concepts once they have been formalised and described mathematically.^[1] But how do we get those mathematical models in the first place? Even translating problems that are already written in mathematical language into a formal language is far from solved.

The process of applying maths

Applied maths can be thought of as a three-step process:

1. Formalise the world. Create a mathematical model, usually with some assumptions that must hold.
2. Match the model to known theory. Map the structure of the domain onto developed pure mathematics.
3. Bring the results back to the real world. What theorems do we know, and what do they mean in this context?

Philosophers of mathematics describe essentially the same structure as an "inferential conception" of applied maths, with three steps: immersion (mapping the physical situation into a mathematical structure), derivation (reasoning inside the mathematics) and interpretation (translating the results back into physical terms).^[2]

How maths has traditionally been applied

So how has maths traditionally been "applied to the real world"? Who did it, and what process or motivation led to the discovery of these applications?

The primary example is the entire field physics. More specifically, the recent (100 or so year) history of electronics shows this pattern well:

• 1861–1865: James Clerk Maxwell published the equations which model electric and magnetic fields. The displacement current was introduced in 1861–62, and the field equations were set out in his 1865 paper.
• 1900–1930: vacuum tubes and differential equations. How do we predict how current flows through a tube as voltages change?
• 1930s–1940s: mathematics meets the PCB. The problem type here involves formalisation (the problem has to be posed mathematically), then optimisation. How do we optimise circuit geometry?

Boolean algebra then became used to model the "digital behaviour" of these circuits.^[3] "Software" was a mathematical abstraction drawn from the hardware.

Software is getting the physical world to do maths

Software is, at its core, getting the physical world to do maths.

A circuit gives us a current or voltage. We can choose to ignore everything about it except that it is a measurement, a real number. And we already have a way of asking questions about real numbers, such as whether $x>y$. Once we decide that a voltage above some threshold counts as 1 and a voltage below it counts as 0, the physical system is doing Boolean algebra.

The engineering side is then about protecting that choice. It has to make sure nothing else in the physical world affects the current and voltage measurements too much, so that the maths stays basically valid. It also has to make sure the other properties of the design are good enough for the device to be usable and useful.

Two directions of applying maths

This suggests there are two directions in which we can apply mathematics:

1. Formalising: turning a real-world system into a mathematical model.
2. Constructing: using that model to build something that doesn't yet exist in the world.

Formalising is where we say, in as concrete terms as possible: "If we assume this thing about the real-world system (e.g. an ammeter in a circuit has zero resistance), then its behaviour is captured exactly by this mathematical model, a set of objects and the relations between them."

The model can be written in any formal language: a system of differential equations, a graph, or a program in a proof assistant like Lean, where the objects are types. What matters is that the description is precise enough to reason about.

Constructing is where we use that formalisation to create new mathematical objects and bring them back into the real world. Concretely, that means using our models of electrical circuit components to design new chips.

Notice that the model captures the idealised real world, not the actual one. The assumptions are what make the match exact, and the real system only satisfies them approximately. So the first step of the whole process is idealising the world.^[4]

The key challenges

The key challenge is choosing an idealised system that we can sufficiently approximate.

An ideal transistor that is on when $I>0.5\text{A}$ and off when $I<0.5\text{A}$ is much easier to approximate than an ideal analog component that produces a range of different output currents at different input currents. The analog component might be more mathematically interesting, and more useful in certain circumstances, but we don't use it to design chips.

Even once we have written down the rules of our idealised system, we still have to make the world adapt so that we can impose those rules onto it. This is sometimes easy: we can standardise the design of ammeters so they have approximately zero resistance. Other times it is hard: we can't easily make people queue in a line at a bus stop for maximum efficiency. It is usually harder when people's preferences are involved.

Back to the bottleneck

Once a system has been idealised and formalised, AI can reason about it. But choosing the idealisation, and then making the world close enough to it for the results to hold, are not things LLMs can currently do. Infrastructure must still be built to make this process happen at scale.

References