AI and Rank 5 mathematics

From Sabine Hossenfelder's Nov. 4 Newsletter:

The past months have proved beyond doubt that today’s AI models are capable of converting their reasoning into symbolic, computer-based maths. The idea of building maths entirely on such computer-readable format is decades old, but now it has come into reach because frontier models can both read and understand the published literature as well as converting it into symbolic proofs.

Mathematician Jared Duker Lichtman at Stanford University in the US has launched the Mathematics Autoformalization Project (MAP) and estimates that the project will cover all known mathematics optimistically by next year, conservatively in 2 to 3 years. It is not the only such project currently underway. A group at META has a similar initiative called ATLAS and Mathlib calls theirs the Formal Frontier.

It sounds like the objective is to make existing mathematics an object of investigation rather, transforming it from a conceptual mechanism into a object of thought in the matter of Piaget's reflective abstraction, which I discuss in this blog post from 2025. That would give us a Rank 5 mathematics. (Other remarks on Rank 5 thought).

Here's what Hossenfelder thinks:

What could such a formalization be good for? For one thing, it would make it dramatically easier to build on the existing corpus of knowledge. But maybe more importantly, it would allow entirely new forms of meta-mathematical studies that could reveal so-far unknown relations between different areas of maths.

Color me sympathetic.