Written: June 17, 2024
I (in collaboration with my beloved silicon helper, Shalosh B. Ekhad), have been using computers to prove (sometimes difficult) mathematical theorems, for many years. Imagine my great disappointment, when I recently got the April 2024 (v. 61, no. 2) special issue of the Bulletin of the American Mathematical Society, dedicated to the impact of computers on mathematics, whose first article, (by the guest editors) entitled:
Will machines change Mathematics?,
did not mention me at all. Neither was I cited in any of the other articles in that special issue.
Before continuing whining about not being cited, let me first give my own (very short) answer to that question.
Q: Will machines change mathematics?
A: YES, but in COMPLETELY different ways than envisioned in the many articles of that special issue. In particular what is now called "mathematics", in a hundred years, would have a new, derogatory, name akin to astrology and alchemy today (once very respectable mainstreame sciences).
Now back to whining. On second thought, I am really lucky to live in these (relatively) enlightened times. Being a (math) heretic of the current religion called "rigorous pure mathematics" (see below).
Today, lucky me, my punishment is just being ignored.
Indeed, there was no mention of
Rather than having a blow-by-blow response to the well-written (but soon to be obsolete) prose of Granville, Venkatesh, Harris, et. al., let me give an analogy. In Richard Feynman's hilarious book "Surely you are joking, Mr. Feynman" (1985, first edition. p.285) the author narrates:
"One day, two or three of the young rabbis came to me and said, "We realize that we can't study to be rabbis in the modern world without knowing something about modern science, so we
would like to ask you some questions"
Feynman was impressed about their broad-mindedness, and told them to ask their question. The question was:
"Is electricity fire?"
then they elaborated: "In the Talmud it says you're not supposed to make fire on Saturday, so our question is, can we use electrical things on Saturdays? Feynman continued: "I was shocked. They weren't interested in science at all", all they care about is to use science to interpret the Talmud better.
I am equally shocked by the efforts of current mainstreamers to use proof assistants, and logic-based programs, to continue the pernicious Greek, "axiomatic", "Euclidean" tradition, with its obsession with rigorous proofs.
Going back to Kurt Gödel, he not-as-famously meta-proved something much more significant than his so-called "undicadabilty":
Most short (decidable, and hence meanigful [in my sense]) mathematical statements have very long proofs
In other words, if a human, or even machine, can prove it fully rigorously, then it is ipso facto trivial. All interesting theorems in the future, if in luck, would have at best a "semi-rigorous" proof, but most often only empirical, or heuristic proofs, See here. Mathematics will become a science again, and not a religious dogma, or competitive sport (see my essay linked to above).
All the concerns about "proof", and its "verification", voiced by Andrew Granville's essay (from that BAMS special issue) would be moot and even laughable in 100 years.
Get over it, Andrew Granville et al.:
On the positive side, the only essay in that special issue that I really liked and fully endorse (except, I do like to do mental math and memorize facts, just for fun) was Eugenia Cheng's paper. This is a much better use of compuerkind's time.
Acknowledgment: One mainstreamer who does not ignore my "crazy" views is the brilliant Gil Kalai, who mentioned me in his comments on Andrew Granville's essay in his famous blog. Toda raba, Gil!