Re: [isabelle] Help on Proof



Dear Howard,

On Mon, 2010-01-04 at 15:56 -0800, Howard Lee wrote:
> Can Isabelle do a proof for the following recursion:
> 
> a(0)=a(1)=a(2)=1; a(n)=((n^3 - 6 n^2 + 12 n - 7)*a(n - 3) + (-3 n^3 + 15 n^2
> - 25 n + 14)*
>      a(n - 2) + (3 n^3 - 12 n^2 + 15 n - 6)*a(n - 1))/(n (n - 1) (n - 2))
> 
> Prove that, for all n ≥ 1, abs(a(n)-(n+1)/3) < 2/(sqrt(3n)).
> 
> Unfortunately, I don't have the bandwidth to download the software; it would
> be greatly appreciated if somebody could input this into Isabelle and email
> me the output.

Isabelle is an *interactive* proof assistant: while the system offers
some automation, proofs of non-trivial theorems must typically be given
by the user.

Proving the above inequation in Isabelle is certainly possible (provided
it holds in the first place), but seems to be beyond the system's
automatic capabilities for now.  So you (or someone else) would have to
develop a proof interactively.  For this, it might be helpful to spell
out a detailed pen-and-paper proof first.

For further reading, I would suggest the "Tutorial on Isabelle/HOL" (at
http://isabelle.in.tum.de/dist/Isabelle/doc/tutorial.pdf).

Regards,
Tjark






This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.