Email Gateway (Aug 18 2022 at 14:27): Email Gateway (Aug 18 2022 at 14:27):From: Howard Lee <howard.lee.1971@gmail.com>
Hello,
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
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.
Thanks,
Howard
Email Gateway (Aug 18 2022 at 14:32):From: Tjark Weber <webertj@in.tum.de>
Dear Howard,
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
Last updated: Apr 26 2024 at 12:28 UTC