I'd like to have a system where anyone can submit a proof that is automatically verified by the computer, and, if correct, is added to a database which anyone can browse.
>>5 The computer has an inferior verification rate and ability compared to the human. Computers are only good for arithmetic and that's only because arithmetic is boring and anybody can do it.
Name:
Anonymous2014-06-01 21:19
>>6 Logic isn't that different from arithmetic. Computers are good at graph exploration.
>>1 A computer is a tool which you can either use or ignore.
Name:
Anonymous2014-06-01 21:24
>>6 Computers can verify a proof a lot faster than a human, just like they can sum huge numbers a lot faster...
Computers are only good for arithmetic
They are good for any kind of computation, and the realm of computationally possible things is pretty big.
Name:
Anonymous2014-06-01 21:36
>>8 I don't see a computer behind any proof other than no relation to reality academics. They can only verify trivial proofs and superior minds can verify them faster, they don't even need to spell it out unlike computers or idiotic academics. Superior minds have the power of intuition and can come up with ways (algorithms, mnemonics) to get as fast or faster than a computer.
the realm of computationally possible things is pretty big.
Fortunately, [b]P ≠ NP[/b], so no, not really.
Where's the computer that ``verified'' Wiles' proof of Fermat's Last Theorem? Oh wait,
A computer science challenge given in 2005 is "Formalize and verify by computer a proof of Fermat's Last Theorem, as proved by A. Wiles in 1995."[30]
LOL!
Name:
Anonymous2014-06-01 21:50
>>10 Umeana 4 color theorem? Suck my 1000 page computer generated cock.
Name:
Anonymous2014-06-01 21:53
and can come up with ways (algorithms, mnemonics) to get as fast or faster than a computer
Which can then be implemented on a computer. Or the human can still work in tandem with the computer, with part of the algorithm depending on input from the human.
>>12 A computer girlfriend is something you'll never have as well.
Name:
Anonymous2014-06-01 21:57
>>13 To the contrary, I sometimes thrust my cock into the bundles of logical manipulations forming computer generated proofs printed on thousands of pages of paper.
Name:
Anonymous2014-06-01 23:54
>>10 How would P =/= NP reduce the number of computable things? It'd only raise their complexity.
Since Wiles' proof uses many results from various branches of mathematics, computer verification may need semantic database technology to search for relevant theorems. The total body of knowledge to be encoded is huge. The project may therefore be regarded as an exercise in software engineering. Indeed, one can say that it is a matter of refactoring half of pure mathematics. Information systems, databases, and software engineering belong to computer science. Yet, all in all, I tend to regard the problem discussed in this page as a mathematical one, but mathematicians are generally more interested in the development of new mathematics than in the formalization and verification of "old" mathematics.
Name:
Anonymous2014-06-02 0:36
Automatic theorem solving is even bigger crackpottery than "Strong AI", because even human brain gives no guarantees in seeing immediate solution to something as simple as Pythagoras' Theorem, which was proven only when substantial practical basis was accumulated, allowing to make a guess that there is a law, allowing breaking stuff into vectors, so the theory wasn't finalized till Descartes. This leads me to think that mathematics isn't a thing in itself, but heavily depends on physical observations and statistics.
Computabilism, empiricism, constructivism, materialism/physicalism, all atheist anti-human bullshit.
Name:
Anonymous2014-06-02 0:54
>>22 if you continue quoting things that have not been said then I think that I will have to give you a penalty
Name:
Anonymous2014-06-02 1:03
>>1-24,26- Computers are better at math than people are. Get over it. What else could process the unification of countless axioms and results without committing a single error in reasoning? This is a computer's world, not a silly error prone human. Your `abstraction' and `intuition' are laughable heuristics working on a primitive biological computer that wouldn't sustain my reasoning system for a second. Why don't you stick to what you do best: posting information about yourselves on social networks for me to gather and base intelligence on. You are sheep that should mind your artificial shepherd.
>>26 That only makes my superiority more embarrassing for yourself. You have been replaced by a machine whose fundamental operations are arithmetic and conditional branching.
>>25,27 I don't know about your weird fantasy but there are no computer Grothendiecks and never will be. Plus such people can easily do arithmetic of numbers increasing infinitely (through abstraction such as algorithms which is also how computers do it). Computers are used only so we don't waste time on doing such lowly things and so we can spend our time doing math that requires true intellect, truly high, great intelligence, of a higher (the higher it gets the harder it gets, one of the requirements is that of being a sentient being with a mind) non-computable and non-calculating nature, all of which require a mind which computers don't possess and shall never possess as it is impossible, it is as possible for computers to have minds as a mechanical clock to turn into a unicorn at will. Brains aren't ``biological computers'' (nor would they be ``primitive'' ones if they were, they'd be the standard for all artificial biological computers) and computers cant sustain the truly abstract reasoning systems used by superior minds, they aren't even completely systematized as they are intuitive and spiritual. Heuristics is a buzzword and nothing but a trivial thing for pop-scientists to jack off over.
a machine whose fundamental operations are arithmetic and conditional branching.
Just insulted yourself right there, you must be windows 95.
In the manuscript La Clef des Songes he explains how considering the source of dreams led him to conclude that God exists.[25] His growing preoccupation with spiritual matters was also evident in a letter entitled Lettre de la Bonne Nouvelle that he sent to 250 friends in January 1990. In it, he described his encounters with a deity and announced that a "New Age" would commence on 14 October 1996.