Do mathematicians still work on proofs by hand?

[SamRoss]

TL;DR Summary

With automated theorem proving, what is left for mathematicians other than perhaps inputting weird axioms?

With automated theorem proving, what is left for mathematicians other than perhaps inputting weird axioms? Or are the machines not as sophisticated yet as I'm assuming they are?

 

[PeroK]

Summary:: With automated theorem proving, what is left for mathematicians other than perhaps inputting weird axioms?

With automated theorem proving, what is left for mathematicians other than perhaps inputting weird axioms? Or are the machines not as sophisticated yet as I'm assuming they are?

There's not a lot that computers can do on their own.

 

[anorlunda]

With computers able to read text out loud, do you still read using your eyes?

 

[SamRoss]

With computers able to read text out loud, do you still read using your eyes?

Yes, for my own knowledge and enjoyment. I think the more pertinent question would be, "With computers able to read text out loud, does anyone pay you to do it?" To which, of course, the answer would be no.

 

[SamRoss]

There's not a lot that computers can do on their own.

It seems to me like there is. I'm just wondering, when a professional mathematician sits down these days to try to tackle the Goldbach conjecture or the Riemann hypothesis, I imagine they search their own heads for some inspiration first but do they then simply go to some theorem-proving software (perhaps using their ideas to narrow down the computational complexity) or is there still any sense in doing it all by hand?

 

[PeroK]

It seems to me like there is. I'm just wondering, when a professional mathematician sits down these days to try to tackle the Goldbach conjecture or the Riemann hypothesis, I imagine they search their own heads for some inspiration first but do they then simply go to some theorem-proving software (perhaps using their ideas to narrow down the computational complexity) or is there still any sense in doing it all by hand?

A computer can assist in trying to prove these things, but mathematical proofs are not just number-crunching.

 

[berkeman]

Yes, for my own knowledge and enjoyment. I think the more pertinent question would be, "With computers able to read text out loud, does anyone pay you to do it?" To which, of course, the answer would be no.

Not true. I don't listen to "audibles" (what used to be "books on tape"), but my wife does quite a bit, and she says the person reading the book can make the book come to life. Often the author reads their own books for the audibles recordings, and whether it's the author or another professional doing the reading, they are getting paid for it by the readers.

https://www.audible.com/

 

[SamRoss]

Often the author reads their own books for the audibles recordings, and whether it's the author or another professional doing the reading, they are getting paid for it by the readers.

Alright, but that's not really the main point here. People pay for books on tape because they like the way the author sounds. In math, only the content is important.

 

[sysprog]

Validating proofs, e.g. in the 1st-order predicate calculus, is mechanical, and any good programmer can code that; however, doing proofs in the 1st-order predicate calculus is NP-complete, and if you find a general method by which computers can solve NP-complete problems in non-exponential, polynomial, or linear time, then the world owes you big fat favors forever. Oh and, if you do manage to prove that NP=P, I'm not sure that you should tell anyone -- the consequences would be extremely huge, and some ruthless people with a strong stake in the status quo might take a dim view of it.

 

[FactChecker]

Mathematicians do not want to prove random facts. A mathematician starts with something that is worth proving, which he strongly suspects must be true. A computer can not do that.
Often the exact conditions and statement are not clear until the formal proof is completed. Computers can not work with that.
A lot of proofs are done in statements that either do not have formal logic translations or would be impractical to develop an entire formal logic to express them. Computers can not work with that.

 

[Svein]

I am currently (at a very slow rate) trying to prove some sums of odd powers of 1/n. This implies a lot of calculations on fractions, where I find using a computer to check on my calculations a real help. Unfortunately the size of the numbers in the numerator/denumerator have now grown so large that I may have to create my own checking program for fractions (Excel has given up and started converting the integers to floating-point numbers).

Just for fun: One of my partial answers look like this: \sum_{n=0}^{\infty}(-1)^{n}(\frac{1}{(6n+1)^{9}}-\frac{1}{(6n+2)^{9}}+\frac{1}{(6n+3)^{9}}-\frac{1}{(6n+4)^{9}}+\frac{1}{(6n+5)^{9}}-\frac{(-1)^{q}}{(6n+1)^{9}})=(\frac{5452745}{162533081088}-\frac{207913\sqrt{3}}{10713850560\cdot 2^{9}})\cdot \frac{10077694}{10077695}\pi^{9}. Good luck in trying to simplify that!