컴퓨터 지원 증명

컴퓨터 지원 증명은 적어도 부분적으로 컴퓨터에 의해 생성된 수학적 증명입니다.

지금까지의 대부분의 컴퓨터 보조 증명은 수학 정리에 의한 대규모 증명의 실행이었다.그 아이디어는 컴퓨터 프로그램을 사용하여 장시간의 계산을 수행하고 이러한 계산의 결과가 주어진 정리를 의미한다는 증거를 제공하는 것이다.1976년, 4색 정리는 컴퓨터 프로그램을 사용하여 증명된 최초의 주요 정리였다.

인공지능 연구 분야에서도 발견적 검색과 같은 자동화된 추론 기법을 사용하여 수학 정리의 더 작고, 명확하고, 새로운 증명들을 아래에서 위로 만들기 위한 시도가 이루어지고 있다.이러한 자동화된 정리 프로버는 많은 새로운 결과를 증명했고 알려진 ^{[citation needed]}정리에 대한 새로운 증거를 찾아냈다.또한 인터랙티브 증명 도우미는 수학자들이 사람이 읽을 수 있는 증명서를 개발할 수 있게 해주며, 그럼에도 불구하고 이는 공식적으로 정확성이 검증되었다.이러한 증명은 일반적으로 사람이 조사할 수 있기 때문에(로빈스 추측의 증명과 같이 어렵지만) 컴퓨터 지원 증명에 의한 증명에 의한 논쟁적인 의미를 공유하지 않는다.

방법들

수학적 증명에서 컴퓨터를 사용하는 한 가지 방법은 소위 검증된 수 또는 엄격한 수치에 의한 것이다.즉, 수치적으로 계산하면서도 수학적 엄격함을 의미합니다.숫자 프로그램의 설정값 출력이 원래 수학 문제의 해답을 포함하도록 보장하기 위해 설정값 산술 및 포함^[clarify] 원리를 사용한다.이는 예를 들어 간격 산술 등을 사용하여 반올림 오류 및 잘라내기 오류를 제어, 포함 및 전파함으로써 이루어집니다.보다 정확하게는 (${\displaystyle }$+${\displaystyle }$, -${\displaystyle }$,${\displaystyle }$×${\displaystyle }$, /${\displaystyle }$)$${$display$ style ( + , , , \ $times$, / )$$} {\ display ( + , , , ) } 。컴퓨터에서는 각 기본 연산의 결과는 컴퓨터 정밀도에 의해 반올림됩니다.단, 기본연산 결과에 대해 상한과 하한이 제공하는 간격을 구성할 수 있다.그런 다음 숫자를 구간으로 대체하고 이러한 표현 가능한 ^{[citation needed]}숫자의 구간 사이에서 기본 연산을 수행합니다.

철학적 반대

이 섹션은 확인을 위해 추가 인용문이 필요합니다. 신뢰할 수 있는 출처에 인용문을 추가하여 이 기사를 개선하는 데 도움을 주십시오. 소스되지 않은 소재는 이의를 제기하여 제거할 수 있습니다. (2020년 10월) (이 템플릿메시지의 삭제 방법 및 삭제 타이밍에 대해 알아보기)

토마스 티모츠코가 처음으로 반대 의견을 밝히면서, 컴퓨터 보조 증명은 수학계에서 몇 가지 논란의 대상이다.Tymoczko의 주장을 고수하는 사람들은 긴 컴퓨터 보조 증명은 어떤 의미에서는 너무 많은 논리적 단계를 수반하기 때문에 '진짜' 수학적 증명은 아니며 수학자들은 추측된 공리에서 논리적인 추론을 효과적으로 Trus로 대체하도록 요구받고 있다고 믿는다.컴퓨터 프로그램의 오류와 런타임 환경 및 하드웨어 ^[1]결함의 영향을 받을 수 있는 경험적 계산 프로세스의 t.

다른 수학자들은 장문의 컴퓨터 보조 증명은 증명보다는 계산으로 간주되어야 한다고 믿는다: 증명 알고리즘 자체가 유효하다는 것을 증명해야 하며, 따라서 증명 알고리즘의 사용은 단순한 "검증"으로 간주될 수 있다.컴퓨터 지원 증명이 소스 프로그램, 컴파일러 및 하드웨어에서 오류의 영향을 받는다는 주장은 다른 프로그래밍 언어를 사용하여 결과를 복제하는 것뿐만 아니라 컴퓨터 프로그램(2005년에 4색 정리에 성공적으로 적용된 접근법)에 대한 공식 증명을 제공함으로써 해결할 수 있습니다.컴파일러와 컴퓨터 하드웨어가 다릅니다.

컴퓨터 지원 증명을 검증하는 또 다른 가능한 방법은 기계가 읽을 수 있는 형태로 추론 단계를 생성한 다음, 그 정확성을 입증하기 위해 증명 검사 프로그램을 사용하는 것입니다.주어진 증거를 확인하는 것이 증거를 찾는 것보다 훨씬 쉽기 때문에, 체커 프로그램은 원래의 보조 프로그램보다 간단하고, 그에 따라 정확성에 대한 자신감을 얻는 것이 더 쉽다.그러나 다른 프로그램의 출력이 올바른지 증명하기 위해 컴퓨터 프로그램을 사용하는 이러한 접근법은 인간의 이해에 대한 인식된 요구를 해결하지 않고 복잡성의 또 다른 층을 추가하는 것으로 보는 컴퓨터 증명 회의론자들에게는 매력적이지 않다.

컴퓨터 지원 증명에 반대하는 또 다른 주장은 수학적 우아함이 부족하다는 것입니다. 즉, 통찰력이나 새롭고 유용한 개념을 제공하지 않는다는 것입니다.사실, 이것은 기진맥진한 어떤 장황한 증거에 대해서도 진전될 수 있는 논쟁이다.

컴퓨터 보조 증명이 제기하는 또 다른 철학적 문제는 추상적인 수학적 개념의 영역에서 과학적 방법이 순수한 이성의 적용보다 더 중요해지는 준경험적 과학으로 수학을 만들 것인가 하는 것이다.이는 수학이 아이디어에 기초하는지 아니면 형식 기호 조작의 "단순히" 연습에 기초하는지 여부에 대한 수학 내 논쟁과 직접적으로 관련이 있다.그것은 또한 만약 플라톤주의 관점에 따르면, 어떤 의미에서는 모든 가능한 수학적 물체가 "이미 존재하는" 것인지, 컴퓨터 보조 수학이 물리학이나 화학과 같은 실험적인 과학이 아닌 천문학과 같은 관찰 과학인지에 대한 의문을 제기한다.수학계의 이런 논란은 21세기 이론물리학이 너무 수학적으로 변하면서 실험의 뿌리를 남기는 것이 아니냐는 물리학계의 질문과 동시에 일어나고 있다.

실험수학의 신흥 분야는 수학탐구를 위한 주요 도구로서 수치실험에 초점을 맞추면서 이 논쟁에 정면으로 맞서고 있다.

적용들

컴퓨터 프로그램의 도움으로 증명된 이론

이 목록에 포함된다고 해서 컴퓨터 체크에 의한 정식 증거가 존재하는 것이 아니라 컴퓨터 프로그램이 어떤 식으로든 관여하고 있다는 것을 의미합니다.자세한 내용은 주요 기사를 참조하십시오.

판매 개요

2010년, 에든버러 대학의 학자들은 사람들에게 컴퓨터 지원 증거를 통해 만들어진 "그들만의 정리"를 살 수 있는 기회를 제공했다.이 새로운 정리는 ^[12][13]구매자의 이름을 따서 명명될 것이다.이 서비스를 사용할 수 없게 되었습니다.

「 」를 참조해 주세요.

레퍼런스

추가 정보

• Lenat, D.B., AM(1976) : 수학에서 발견을 위한 인공지능 접근법입니다. 휴리스틱 서치, 박사.논문, STAN-CS-76-570 및 경험적 프로그래밍 프로젝트 보고서, HPP-76-8, 스탠포드 대학, AI 연구실, 캘리포니아주 스탠포드.
• Meyer, K. R., & Schmidt, D. S. (2012년)컴퓨터 보조 분석 증거Springer Science & Business 미디어.
• Nakao, M. Plum, Y. Watanabe(2019) 편미분 방정식에 대한 수치 검증 방법 및 컴퓨터 보조 증명(계산 수학의 스프링어 시리즈).

외부 링크

• Oscar E. Lanford: "파이겐바움 추측의 컴퓨터 지원 증거", Bull. 아머. 수학. 사회학회, 1982년
• 에드먼드 퍼스AM은 왜 힘이 다 빠졌지?
• 컴퓨터에 의해 수행된 숫자 교정 오류가 발생할 수 있습니다.
• "A Special Issue on Formal Proof". Notices of the American Mathematical Society. December 2008.