리만 가설이나 골드바흐 추측 같은 것들을 일차논리 문장으로 번역한 다음에 페아노공리계 혹은 ZFC에서 증명가능한 문장들을 판별해주는 프로그램(물론 결정불가능하겠죠)에 넣어서 돌리다 보면 대충 그 프로그램의 시간 복잡도에 의하면 x시간 안에 답이 나와야 한다고 알 수 있는데 계속 돌아가는 걸 보니까 결정불가능한 문장이구나! 하고 경험적인 방법으로 유추해볼 수 있는 날이 오지 않을까요?
아니면 기계가 증명을 해줄 수도 있겠죠?