TY - RPRT TI - Auto formalisation of Chaitin and of the surprise incompleteness Theorem AU - Thierry Coquand PY - 2026 UR - https://arxiv.org/abs/2606.12462 ID - 2606.12462 ER -