Math writing is dull when it neglects the human dimension

I'm sorry, but that's just naive techno-solutionism. Maybe the computer will be able to solve your syntax problems, i.e., write proofs. It will never know anything about the semantics.

Said differently. Maybe the computer will be able to give you a proof on demand on statement number 123456789 in some Gödel numbering of statements. What it won't be able to tell you is that the theorem should be called the "intermediate value theorem" and what it means. Math isn't just coming up with formally correct proofs for pre-existing statements.

I also don't see what "P vs NP" has to do with anything.

> Today, most of the math is figuring out how to solve an equation, i.e. to give an algorithm to calculate the solution. We then "quantize" the algorithm to a state machine (e.g. convert reals to floats, algorithm steps to machine code), so that we could run the state machine on a computer and get a result.

I'm a mathematician. What you wrote is just bonkers. Some parts of math are about writing algorithms to solve equations. The vast majority of math isn't.

But (not joking here) this is a perfect opportunity for an LLM -- two opportunities, actually.

LLM A takes a dry paper and gives it context. It could make up the context but a good one would look up and offer an anecdote from Riemann's life or something. I see nothing wrong with that.

And LLM B could take a paper with that stuff, which to me is fluff, and strip it all out, leaving the dry bones for me to pick over and savour.

It would really just be another form of language translation, if a higher level one.

And this is at the heart of P vs NP question, how to solve SAT, and once we understand that, all the math that is about solving equations (i.e. that of practical value) will become very boring. Kinda like when a game becomes solved with a computer.

(This reminds me of Chomsky and Norvig debate on the machine learning and nature of understanding. I wouldn't think I would take Norvig's position, yet here we are.)

Addendum: I am also not arguing that computers writing proofs are a necessity for this, but rather efficiently (as possible) solving SAT instances. You don't need to state a hypothesis (and thus prove it) for an infinite number of cases to solve practical problems.

I am also not judging value of math - yeah, it is fun. All I am saying it inherently has a human dimension in the sense we don't need it (assuming we have an efficient SAT solver) to solve practical problems.

Over time it will probably grow into long-long editorial pieces. I will propably have to use AI to strip down the story mode.