Mathematics was developed as a strong research instrument with fully verifiable argumentations. We call any formal theory based on syntactic rules that enables to algorithmically verify for any given text whether it is a proof or not algorithmically verifiable mathematics (AV-mathematics for short). We say that a decision problem L is almost everywhere solvable if for all but finitely many inputs x one can prove either "x in L" or "x not in L" in AV-mathematics.

First, we prove Rice's theorem for unprovability, claiming that each nontrivial semantic problem about programs is not almost everywhere solvable in AV-mathematics. Using this, we show that there are infinitely many algorithms (programs that are provably algorithms) for which there do not exist proofs that they work in polynomial time or that they do not work in polynomial time. We can prove the same also for linear time or any time-constructible function. This explains why proving superlinear lower bounds on the time complexity of concrete problems may be really hard. Moreover, we prove that there are infinitely many algorithms for which one cannot decide in AV-mathematics whether they solve SATISFIABILITY or not.

Note that, if P != NP is provable in AV-mathematics, then for each algorithm A it is provable that "A does not solve SATISFIABILITY or A does not work in polynomial time". Interestingly, we finally show that there exist algorithms for which it is neither provable that they do not work in polynomial time, nor that they do not solve SATISFIABILITY. Moreover, there is an algorithm solving SATISFIABILITY for which one cannot prove in AV-mathematics that it does not work in polynomial time.

Furthermore, we show that P = NP implies the existence of algorithms X for which the claim "X solves SATISFIABILITY in polynomial time" is not provable in AV-mathematics. Analogously, if the multiplication of two decimal numbers is solvable in linear time, one cannot decide in AV-mathematics for infinitely many algorithms $X$ whether "X solves multiplication in linear time".