Constructive Mathematics with the Predicate of the Current Mathematical Knowledge

We assume that the current mathematical knowledge K is a finite set of statements from both formal and constructive mathematics, which is time-dependent and publicly available. Any formal theorem of any mathematician from past or present forever belongs to K. We assume that mathematical sets are atemporal entities. In this article, they exist formally in ZFC theory although their properties can be time-dependent (when they depend on K) or informal. Algorithms always terminate. We explain the distinction between algorithms whose existence is provable in ZFC and constructively defined algorithms which are currently known. By using this distinction, we obtain non-trivially true statements on decidable sets X ⊆ N that belong to constructive and informal mathematics and refer to the current mathematical knowledge on X.