I apologize for my bad example. The following Lisp program (domain binary search) produces an approximation to a zero of f(x) at 1 bit per iteration: (defun intval (f lb ub n) ;;; Produce n'th approx to zero of f(x) in interval lb<x<ub. ;;; f(lb)<0<f(ub). (assert (minusp (funcall f lb))) (assert (minusp (- (funcall f ub)))) (cond ((minusp n) `(,lb ,ub)) ((< lb ub) (let* ((ib (/ (+ lb ub) 2)) (fib (funcall f ib))) (cond ((zerop fib) `(,ib ,ib)) ((minusp fib) (intval f ib ub (1- n))) (t (intval f lb ib (1- n)))))) (t `(,lb ,ub)))) At 09:04 AM 11/15/2011, Henry Baker wrote:
Well, if someone shows you an x0 such that f(x0)=0, then the verification is trivial; finding that x0 might have taken eons, but once it has been found, it is easily verified.
So the intermediate value theorem is still an example for you.
At 08:55 AM 11/15/2011, Marc LeBrun wrote:
="Henry Baker" <hbaker1@pipeline.com> Aren't most proofs of the "intermediate value theorem" essentially non-constructive?
I again apologize for not being clear what I was asking for--I buried the second half of the conjunction too deeply in the prose:
=Marc LeBrun ... a non-constructive proof... that ALSO has an easily-verified case?
Come to think of it factoring provides an example: you can easily and non-constructively show that some big N is composite, AND you can easily verify that some X divides N, BUT finding X is hard.
Thanks for all the suggestions!