The Kochen-Specker theorem shows the impossibility for a hidden variable theory to consistently assign values to certain (finite) sets of observables in a way that is noncontextual and consistent with quantum mechanics. If we require noncontextuality, the consequence is that many observables must not have pre-existing definite values. However, the Kochen-Specker theorem does not allow one to determine which observables must be value indefinite. In this paper we present an improvement on the Kochen-Specker theorem which allows one to actually locate observables which are provably value indefinite. Various technical and subtle aspects relating to this formal proof and its connection to quantum mechanics are discussed. This result is then utilized for the proposal and certification of a dichotomic quantum random number generator operating in a three-dimensional Hilbert space.

The Kochen-Specker theorem proves the inability to assign, simultaneously, noncontextual definite values to all (of a finite set of) quantum mechanical observables in a consistent manner. If one assumes that any definite values behave noncontextually, one can nonetheless only conclude that some observables (in this set) are value indefinite. In this paper, we prove a variant of the Kochen-Specker theorem showing that, under the same assumption of noncontextuality, if a single one-dimensional projection observable is assigned the definite value 1, then no one-dimensional projection observable that is incompatible (i.e., non-commuting) with this one can be assigned consistently a definite value. Unlike standard proofs of the Kochen-Specker theorem, in order to localise and show the extent of value indefiniteness, this result requires a constructive method of reduction between Kochen-Specker sets. If a system is prepared in a pure state $\left|\mathrm{\psi }\right.〉$ , then it is reasonable to assume that any value assignment (i.e., hidden variable model) for this system assigns the value 1 to the observable projecting onto the one-dimensional linear subspace spanned by $\left|\mathrm{\psi }\right.〉$ , and the value 0 to those projecting onto linear subspaces orthogonal to it. Our result can be interpreted, under this assumption, as showing that the outcome of a measurement of any other incompatible one-dimensional projection observable cannot be determined in advance, thus formalising a notion of quantum randomness.

In contrast with software-generated randomness (called pseudo-randomness), quantum randomness can be proven incomputable; that is, it is not exactly reproducible by any algorithm. We provide experimental evidence of incomputability\char22{}an asymptotic property\char22{}of quantum randomness by performing finite tests of randomness inspired by algorithmic information theory.