Abstract: Cristian Calude

CAN PEANO ARITHMETIC PROVE RANDOMNESS?

 

 

           We prove that every computably random real is provable in Peano Arithmetic(PA) to be random. The results are true for the more general class of c.e. epsilon-random reals.

           The talk will present both the mathematical results and their formalization using the proof-assistant Isabelle.