Where is the fashionable mathematics?

I'm not the ideal person to ask, never having published a novel mathematical result and not having particularly deep knowledge of math, but I understand "formal" in this context to mean "mechanical". A formal manipulation of symbols is, as I understand it, one that you can carry out without attaching any meaning to the symbols you are manipulating.

This is not the same thing as "rigorous", because it's entirely possible for a formal manipulation to be unsound (with respect to some theory). For example, suppose you want to prove that a left multiplicative identity is also a right identity; that is, ∀x: 1·x = x ⇒ ∀x: x·1 = x. You can apply commutativity and rearrange the symbols to get a proof — that's a purely formal technique, and it's correct and rigorous for, say, complex-number multiplication. But if you're thinking of some other multiplication operations, like that of square matrices of some size, or of quaternions, that's not a rigorous proof, because those multiplication operations aren't commutative. (But in those cases it turns out to be a correct theorem anyway, because they are associative.)

Compiling a program is another operation that is formal but rarely rigorous.

The hope of using proof assistants in math is that by formalizing our reasoning, we can also make it more rigorous, with the aid of computers and a great deal of cleverness. Most mathematicians are not yet convinced.

If you're using a proof assistant, you can't just write something like "X clearly follows from Y" or "Z is left as an exercise to the reader": you have to specify every step, even if they're steps a human reader would easily figure out themselves.

The biggest pain point with the theory was its handling of equality, which HoTT fixes.

Ergonomically.. well it's hard to describe TBH, the easiest way to see is to just download one of these systems and try using them. You try to prove a theorem and everything just ends up taking way longer than you'd expect. Mostly because you can't gloss over small details the way mathematicians will do informally. Every small turn of phrase like "for large enough N" or "without loss of generality" can become dozens of extra lines of code.

I was being intentionally provocative. On the other hand I feel like there are plenty of people in my (mathematics) department who would say that "normal" fields like geometry, topology, algebra, number theory and analysis are where the action is happening, and category theory is just a tool which we use to get "normal" maths done. On the other hand now Scholze is beginning to use infinity categories more in his work, this might change -- but it might not. Maybe in 10 years time there will be a book "infinity categories for the working mathematician" which we all read the first ten pages of and this is all that most of us need. Note that category theorists like Hyland and Johnstone have retired from Cambridge now and have not been replaced -- in the UK now you are more likely to find a category theorist working in a computer science department than a mathematics department. Whether or not it is "real mathematics", it is certainly a fact that in the UK at least it is an extremely small community, whereas our departments are full of number theorists, geometers, topologists, analysts and algebraists all of whom need to know essentially no category theory beyond the basic language of adjoint and representable functors.

I disagree that all knowledge, or even the most important items of knoknowledge, are reducible to mathematics.

While this is factually true, as a normative statement it represents an inversion of priorities, like attending school so that you can have a summer vacation, admiring Michelangelo's art because of how much reputation the Medicis gained by patronizing it, or hoping your mother will get a better job so that she can buy you more candy. It trivializes mathematics.

It's true that we only have cryptography, computers, physics, and finance — and not only the modern kind — because of the human study of mathematics. But cryptography and finance are of distinctly tertiary importance, computers and physics of secondary importance, and mathematics of primary importance. So it is nonsense to say that mathematics is important because it helps us understand physics. Mathematics is important because it transcends physics; the same mathematical theories would be consistent in a universe with totally different physics. Their beauty does not depend on whether or not they happen to describe the physics in a particular universe or not.

The Pythagorean Theorem was discovered by the humans in Mesopotamia somewhere between 3500 and 5000 years ago; nobody knows who discovered it. (Pythagoras wouldn't be born for centuries.) It was used to design buildings, but the buildings have been worn to dust. It was used then to divide up farmland, but the farmers are dead, their bones have worn away to dust in the sand, their names are mostly forgotten, and their farmland turned to desert. But the knowledge of the theorem, and the place-value number system the Babylonians invented, has endured, and the humans still divide the circle into 360 degrees, each degree into 60 minutes, and each minute into 60 seconds, a tradition inherited from the Babylonians.

Moreover, the stars and planets have moved in a way described by the Pythagorean Theorem since there have been planets and stars, for almost 14 billion of the time unit that would eventually be a "year" on Earth. And, most likely, they will continue to do so for as long as there are planets and stars; and as long as there are humans, they will know the Pythagorean Theorem, even if the name of Babylon is forgotten.

Today the humans consider cryptography important because it governs the rise and fall of nations and empires; they consider finance important because it governs the rise and fall of firms, and decides which humans are powerful and which humans are poor and starving. But, it is nearly certain that all of those powerful humans will be dead in a century and a half, and all of those nations and empires will be gone in a millennium.

But, if libraries survive, so too will the knowledge of group theory, and of linear algebra, and of computability theory.

From the point of view of anyone in 5000 CE or 10000 CE, it will seem absurdly short-sighted that someone in 2020 CE thought that the important thing about elliptic curves was that cryptography based on them permitted long-forgotten nations like Russia to achieve informatic independence from the long-forgotten United Nations of America, because they were not yet to discover the Elliptic Curve Discrete Log Algorithm for 440 more years, and didn't have large quantum computers yet.

I say that physics and computers are less insignificant than cryptography and finance because knowledge of physics does progressively improve, and is objective, like that of mathematics; and computers both serve to advance knowledge of mathematics, and are themselves imperfect realizations of abstract mathematical objects, what is often called automata theory. But certainly questions like how to get CUDA to run properly with a particular model of Tesla card, or which versions of Blink support Webfonts, are of no importance at all from the standpoint of 5000 CE or 10000 CE — but the Halting Problem will still be uncomputable, long after Turing's name is forgotten.

Physics theories, though, are historically contingent and provisional in a way that mathematical theories are not. The quantum theory of probability is, as Aaronson's book explains, an internally self-consistent extension of probability theory to the complex plane entirely apart from its use to describe the behavior of light, electrons and so on. Theorems can be proven within its axiomatic system, and those theorems will continue to hold even when the humans learn how it fails to describe the contingent reality of this universe. So, again, mathematics is eternal, at least until the libraries are burned, and exact; physics is a provisional approximation, until a better approximation is found.

(For a much more cynical perspective on the humans, see https://news.ycombinator.com/item?id=22393163.)

It's quite ironic. Imaginary numbers are quite real, but real numbers are quite imaginary.

What is good, Wolff, and what is not good? How do we know these things?