https://en.wikipedia.org/wiki/Proof_assistantProof assistant - WikipediaProof assistant - Wikipediaen.wikipedia.org
올해 5월 쯤 Github 에, 다음을 증명하는 글이 올라왔더라.
BB(5)=47,176,870
https://github.com/ccz181078/Coq-BB5GitHub - ccz181078/Coq-BB5Contribute to ccz181078/Coq-BB5 development by creating an account on GitHub.github.com
(함수 BB는 바쁜 비버 함수. BB의 엄밀한 정의는 위 링크에 있음)
훑어보니까, Coq 라는 증명 보조 프로그램을 사용했더라고.
느슨하게 말해서,
이건 'Coq 실행 결과는 항상 버그가 없다'를 공리로 하는 거잖아?
저 공리를 증명하는 것도 불가능하고.
이런 증명 보조기를 이용한 증명에 대해,
수갤러들은 어떻게 생각해?
아직까지 검토는 사람 몫이지
공리는 저런데 붙이는 말이 아님 사람의 검토는 항상 옳다 이런걸 공리라도 만들어서 쓰고있는거야?
표현을 이렇게 바꾸면 어때? 'Coq 프로그램이 항상 소스 코드로 명세된 이론적인 절차대로 동작한다면, 임의의 입력에 대한 Coq 실행 결과는 모두 타당하다'
4색정리랑 뭐가 다름. 오류 없으면 맞겠지 - dc App
컴파일러 무결성은 이리저리 다루지 않나? Coq/lean은 이미 체크되어있을거같은데
증명 불가능하다고 생각하는 이유가 뭐임?
'정지 문제' 때문에 증명 불가능하다고 생각했어. 그런데 지금 생각해보니, 저 논문에는 Coq가 유한한 실행 시간 안에 결과를 출력하는 입력들만 존재하겠네.
이 문서에서 내가 '공리'라고 표현한 명제를, 내 노력껏 형식화 해보면 다음과 같아. - Coq 설명서대로 동작하는 이론적인 프로그램을 CoqA 라 하자. - Coq 소스 코드대로 동작하는 이론적인 프로그램을 CoqB 라 하자. - "프로그램 x가 문서 y를 입력으로 받아, 'y는 타당하다'는 결과를 출력했다"를 "Valid(x, y)" 라 표현하자. - "프로그램 x가 문서 y를 입력으로 받아, 'y는 타당하지 않다'는 결과를 출력했다"를 "Invalid(x, y)" 라 표현하자. - 이 경우에, 다음 문장 1, 2가 모두 참이다. 1. ∀y (Valid(CoqA, y) ↔ Valid(CoqB, y)) 2. ∀y (Invalid(CoqA, y) ↔ Invalid(CoqB, y))