Lean으로 콜라츠 추측 반증했다는 증명, 커널 버그로 판명나며 프루프 오브젝트 논쟁 재점화 · cho.sh