I've been thinking about creating a platform to help others learn mathematics.
This platform would use some custom made programming language to write some problems and its solutions.
The problem with such a project, is that it would be pretty difficult to test the correctness of the solutions proposed by the players, so I thought I could just use some examples, and run these algorithms against the examples, and if all pass, to consider the want-to-be-proof as valid. This obviously would not really prove the correctness of the algorithm, but it's a start.
I've been trying to find some examples of theorems and algorithms (which would try to prove them) which work for, for example, really nicely behaved function, but fail for weird ones.
To be more concrete, here's an example of a problem and attempted solution that could appear:
$\bf Problem$
Let $f:[a,b] \to \Bbb R$ be continuous. Prove that if $f(a)<0$ and $f(b)> 0$, then there exists some $c\in (a,b)$ such that $f(c)=0$.
The standard proof of this theorem simply calculates the midpoint of both ends of the interval and does a (sort of) binary search, possibly taking infinitely many steps.
$\bf Algorithm$
(Code written in pseudo-ruby, I'm not sure it's correct, but that's not the point)
$\bf Solution\ testing$
For the given example, I would have a set of continuous functions, like $\{x\mapsto x^2, x\mapsto \sin(x), x\mapsto \exp(x^3), \text{etc} \}$, and would use some random choices of $a, b$, and run for each of these, $\text{find_zero}(f,a,b)$, and this would pass the test if $|f(\text{find_zero}(f,a,b))|<\epsilon$ for some small $\epsilon$.
As said before, can you think of any example where some standard algorithm would pass the test for all nice examples but would fail for a strange function?
$\bf\text {Take into consideration, that I'm looking for "relatively simple" algorithms}\\ \text{ (i.e, algorithms that someone would be able to write in some programming language).}$
While I appreciate your intent, and I hate to be that guy, but I must say that this whole approach is extremely unsatisfying to me as a way of helping others to learn mathematics (which is, after all, your stated goal). Particularly as regards your example theorem.
First, observe that the IVT is false on the rationals: if for example we let $f(x) = x^2 - 2$, then $f: \mathbb{Q} \rightarrow \mathbb{Q}$ is continuous, but there is no $q \in \mathbb{Q}$ for which $f(q) = 0$. And yet we can still 'bracket' $0$ with pairs $(a,b)$ such that $-\epsilon < f(a)< 0 < f(b) < \epsilon$ for any arbitrarily small $\epsilon \in \mathbb{Q}$.
This should tell you that something is missing in your informal description of the 'standard proof'. There is something quite special about $\mathbb{R}$ that is lacking in $\mathbb{Q}$ which is fundamental to the proof of IVT for $\mathbb{R}$.
Then on point to your post: your proposed 'verification' function is then trying to 'verify' something that is true on the reals, but false on the rationals. And the IEEE 754 floating point definition (which is what all your arithmetic functions and their compositions will rely on) is an even crappier version of $\mathbb{R}$ than $\mathbb{Q}$ - it doesn't even ensure that $\forall x < y, \exists z: x < z < y$.
To the extent that 'find_zero()' 'verifies' that IVT (or any other such theorem $T$ for that matter) is true in $\mathbb{R}$, might they not also simultaneously incorrectly 'verify' IVT (or $T$) is true in $\mathbb{Q}$?
It all just seems quite misleading at best, no matter what the results are!