Seemingly Impossible Lean Programs [draft]
Introduction - Infinite search in finite time It should come as no surprise that an exhaustive search over a finite set can be performed algorithmically by enumeration. On the other hand, it is impossible to perform such an exhaustive enumeration over the natural numbers or the integers, as these sets are infinite. However, somewhat paradoxically, there are infinite sets that can be exhaustively searched in finite time. More precisely, there is at least one infinite set $X$ with the property that for any given Boolean-valued function $p$ on $X$, it is possible to algorithmically verify within finite time whether $p$ holds for all elements of $X$ or to produce a counter-example if one exists....