QED 매니페스토

QED 매니페스토는 모든 수학 지식을 컴퓨터 기반으로 한 데이터베이스로, 엄밀하게 공식화되었고 모든 증거가 자동으로 확인되었습니다. (Q.E.D.는 라틴어로 "시연될 예정"이라는 의미)")

개요

이 프로젝트에 대한 아이디어는 주로 로버트 보이어의 추진력으로 1993년에 나왔다.이 프로젝트의 목표는 가칭 QED 프로젝트 또는 프로젝트 QED로 명명되었으며, 여러 ^[1]연구자들의 의견을 받아 1994년에 처음 발행된 문서인 QED 매니페스토에 요약되어 있습니다.노골적인 저작권은 의도적으로 피했다.전용 메일링 리스트가 작성되어 QED에 관한 2개의 과학 컨퍼런스가 개최되었습니다.첫 번째 컨퍼런스는 1994년에 Argonne 국립 연구소에서 개최되었고, 두 번째 컨퍼런스는 1995년에 Mizar 그룹이 ^[2]조직한 바르샤바에서 개최되었습니다.

이 프로젝트는 1996년까지 논의와 계획 이상의 성과를 거두지 못한 채 해체된 것으로 보인다.2007년 논문에서 Freek Wiedjk는 프로젝트 ^[3]실패의 두 가지 이유를 밝히고 있습니다.중요도 순서:

• 수학의 공식화를 연구하는 사람은 거의 없다.완전 기계화된 수학에는 설득력 있는 응용 프로그램이 없다.
• 공식화된 수학은 아직 진짜 전통적인 수학과 닮지 않았다.이것은 부분적으로 수학 표기법의 복잡성, 그리고 부분적으로 기존의 정리 계산자와 증명 보조자의 한계 때문이다; 이 논문은 주요 경쟁자인 미자르, 홀, 그리고 Coq가 수학을 표현하는 능력에 심각한 단점을 가지고 있다는 것을 발견한다.

그럼에도 불구하고 QED 스타일의 프로젝트는 정기적으로 제안됩니다.미자르 수학 도서관은 학부 수학의 많은 부분을 공식화하고 있으며,^[4] 2007년에는 가장 큰 도서관으로 여겨졌다.유사한 프로젝트로는 메타매스 프루프 데이터베이스와 ^[5]린으로 작성된 mathlib 라이브러리가 있습니다.

2014년 QED^[6] 매니페스토 워크숍의 20년은 Vienna Summer of Logic의 일환으로 조직되었습니다.

「 」를 참조해 주세요.

• 형식주의 (수학)
• 수리 지식 관리
• POPLmark, 프로그래밍 언어 이론의 보다 온건한 프로젝트

레퍼런스

추가 정보

• H. 바렌드레그 & F.Wiedjk, The Challenge of Computer Mathematic, Transactions A of the Royal Society, 1835년 제363호, 2351년–2375년, 2005년
• "A Special Issue on Formal Proof". Notices of the American Mathematical Society. December 2008. (오픈 액세스 문제)
• 리처드 A. De Millo, Richard J. Lipton, Alan J. Perlis, 정리 및 프로그램의 사회과정과 증명, ACM의 커뮤니케이션, 제22권, 제5호(1979년 5월), 페이지: 271 ~ 280
• John Harrison, 형식화된 수학, 테크니컬 리포트 36, Turku 컴퓨터 사이언스 센터(TUCS)
• Itay Weiss, The QED Manifesto © Version 2.0, Journal of Software vol. 11, 8, 페이지 803-815, 2016.

외부 링크

• Freak Wiedjk, 100개 이론 공식화 100개 공통 이론의 공식화 진행 상황을 추적하는 페이지.
• Freak Wiedjk, The Sevention Provers of the World, 17명의 다른 증명 보조원 중 2명의 제곱근의 불합리한 증거입니다.
• 공식화된 수학은 미자르 증명서가 제시되는 저널이다.
• 공식 교정 자료 보관소는 Isabelle/HOL에 있는 유사한 교정 자료 저장소입니다.
• [1] Coq의 증거 저장소.
• UniMath "Coq 라이브러리는 일가의 관점을 사용하여 실질적인 수학 체계를 공식화하는 것을 목표로 합니다."