18
$\begingroup$

Motivation: I'm writing a proof, and within it, I need to prove:

Conjecture: Let $p$ be an odd prime (i.e. $p \neq 2$). Let $c \geq 2$, $d \geq 1$ and $r \geq 1$. If $p^r$ divides $cd$, then $d(c-1) \geq r+1$.

This conjecture, should it prove to be true (and I suspect it will [it seems to be like "prove elephants are bigger than mosquitos"], unless I've missed a few small cases), would be a rather uninteresting result and no real insight into the problem I'm studying. This leads me to the question:

Question: Does there exist a software package that would allow me to automatically prove (or disprove) this conjecture (or results like this)?

  • 4
    I know this website with lots of very helpful people who would like to earn reputation points...2011-03-10

2 Answers 2

8

You may want to look into the proof assistant Isabelle. It's freely available under a BSD license, and is a start towards the sort of thing your looking for. It's an interactive theorem proving environment that offers a language, Isar, for expressing formal proofs, some built in automated tools, and a sledgehammer tool that will run several external automated theorem provers in parallel. However, I have only just begun to use this system this week, so I am unable to verify for myself if it can handle the simple proof from your question.

This paper outlines the work that went into producing a formally verified proof of the prime number theorem using Isabelle. The authors discuss some of the difficulties they had in proving small lemmas, but they seem confident that the available automated tools will eventually be strong enough to handle these sorts of things. Since this paper was written in 2005, it's conceivable that sufficiently strong tools are available today, but I am unaware of the extent of Isabelle's current capabilities.

Edit: With some coaxing, I was able to produce a partially automated proof of your result using Isabelle. I found it more challenging to get Isabelle to prove this result than to simply prove it myself though. At the moment this probably isn't a practical means of saving labor. Perhaps someone expert in this system with access to a wider library of relevant theorems and lemmas could automate the proofs of a wide class of routine results, but I don't think the functionality you want is quite there yet. Nevertheless, you might find it more fun to try to get a computer to check an apparently routine conjecture than to try to grind through a proof yourself.

0

Isabelle can prove theorems mechanically, but it can prove very little theorems that need human creativity. Because Peano arithmetic is undecidable, although sound but not complete theorem provers can be built using some techniques, this kind of theorem provers are usually very weak and cannot handle really non-trivial theorems.

The field of theorem proving is waiting desperately for breakthrough.