Fixing existing proofs is the key roadblock. Furthermore automated proof techniques would have different amounts of utility in different parts of math. And finally, most mathematicians like understanding their proofs. Automated proofs don't tend to be understandable. It is like the endgame studies that computers did in chess - you can see that it works, but you can't see how anyone could think of or remember it. (Which is why no human had thought of it...)
Incidentally your playing around with the Peano axioms mislead you. The Peano axioms allow you to reason about the positive integers. (Proving that every positive integer is either even or odd is simple induction.) To get from there to the integers, you model each integer as an equivalence class of pairs of integers (p, n) with (p, n) in the same equivalence class as (p', n') if p'+n = p+n'. (Think of (p, n) as p-n.) Now you have to prove that the equivalence relation is well-defined, and that definition of addition is likewise. Define the usual multiplication, and prove that that works. And that you can map the positive integers into the integers with p->(p+1, 1). Then you can start proving other things, such as that every integer is either positive or negative.
Once you have all of that, then you're in a position to prove things about the integers (like every integer is even or odd).
You have to go through the same process again to define rationals as equivalence classes of pairs of integers. You can then define real numbers as equivalence classes of Cauchy sequences of rationals. Once you've done that you then have to reprove everything. But, amazingly, you can get all of the way through Calculus with just the Peano axioms. (It takes a lot of work though.)
Posts are HTML formatted. Put <p> </p> tags around your paragraphs. Put <code> </code> tags around your code and data!
Titles consisting of a single word are discouraged, and in most cases are disallowed outright.
Read Where should I post X? if you're not absolutely sure you're posting in the right place.
Please read these before you post! —
Posts may use any of the Perl Monks Approved HTML tags:
You may need to use entities for some characters, as follows. (Exception: Within code tags, you can put the characters literally.)
- a, abbr, b, big, blockquote, br, caption, center, col, colgroup, dd, del, div, dl, dt, em, font, h1, h2, h3, h4, h5, h6, hr, i, ins, li, ol, p, pre, readmore, small, span, spoiler, strike, strong, sub, sup, table, tbody, td, tfoot, th, thead, tr, tt, u, ul, wbr
Link using PerlMonks shortcuts! What shortcuts can I use for linking?
See Writeup Formatting Tips and other pages linked from there for more info.
| & || & |
| < || < |
| > || > |
| [ || [ |
| ] || ] ||