5 ms·
I thought everyone knows that Hilbert proved that it's impossible for machine to prove any theorem that human don't already know...
by jewelry 8y ago
I thought everyone knows that Hilbert proved that it's impossible for machine to prove any theorem that human don't already know...
- digama0 8y agoOnly if you're an ideal rational agent. Maths is hard.
- smadge 8y agoThe proofs in Metamath are not produced by machines. Humans write them, but machines validate them.
- Someone 8y agoThat’s incorrect. It is easy to write a program that can prove any mathematical theorem that has a finite proof. The only limitations will be speed (very, very much so) and running out of memory. The latter will always happen when the to be proven theorem is false or undecidable. To see why that works, consider that any mathematical proof can be written in a fixed alphabet, and will be of finite length, in a proving language in which proofs can be machine-checked in finite time. Assuming that, to prove a theorem T, loop over all strings (possible because there are countable infinite of them. An implementation will do this by increasing length of the strings), and check for each of them whether it’s a valid proof for T (an extension can check whether it’s a proof for not-T, and exit if it is) Alternatively, to find _all_ valid theorems, loop over all strings, and check for each of them whether it’s a valid proof (that will find many, many extremely dull theorems, but assuming such theorems exist, it will find beautiful ones humans haven’t thought of, too)
- DoctorOetker 8y agothats just utter nonsense. furthermore what would have been this magic time of "already" ? that alone should have triggered your own bs alert...