How to run algorithmic information theory on a computer: Studying the limits of mathematical reasoning