증명 (수학)

수학에서 증명(證明, 영어: proof)은 공리와 주어진 가정으로부터 어떤 명제가 성립함을 연역적으로 보이는 논증이다. 증명에서는 정의와 추론 규칙, 이미 증명된 정리를 이용하여 결론을 이끌어 낸다. 여러 사례에서 명제가 성립한다는 관찰과 달리, 증명은 그 명제가 주장하는 범위 전체에서 결론이 성립하는 근거를 제시한다.

증명은 보통 자연어와 수식, 도형을 이용하여 서술된다. 직접적인 추론, 귀류법, 수학적 귀납법 등 여러 방법이 쓰이며, 하나의 증명에서 여러 방법을 결합하기도 한다. 증명은 명제의 정당화뿐 아니라 성립 이유의 설명, 새로운 결과의 발견, 이론의 체계화와 지식의 전달에도 기여한다.

수리논리학에서는 언어와 추론 규칙을 명시하여 증명을 형식적인 대상으로 다룬다. 이러한 증명의 구조와 성질을 연구하는 분야가 증명 이론이며, 증명의 형식화는 컴퓨터를 이용한 검증에도 사용된다. 어떤 명제를 증명할 수 있는지는 채택한 공리와 논리 체계에 의존하며, 특정 공리계에서 명제와 그 부정 가운데 어느 쪽도 증명할 수 없는 경우도 있다.

정의와 논리적 구조

전제와 결론

증명은 출발점으로 삼는 전제와 그로부터 얻으려는 결론을 구별한다. 공리는 해당 이론에서 증명 없이 출발점으로 채택하는 명제이고, 정의는 용어나 기호의 뜻을 정한다. 증명 과정에서 이미 얻어진 정리를 사용할 때에는 그 정리의 가정이 충족되는지도 확인해야 한다. 예를 들어 실수 $x$에 대해 $x^{2}>0$을 결론으로 얻으려면 $x\neq 0$이라는 조건이 필요하다.

함의 $P\Rightarrow Q$의 증명은 $P$가 성립한다는 가정 아래에서 $Q$가 따라옴을 보이는 것이다. 이때 $P$ 자체가 언제나 참이라고 주장하는 것은 아니다. 또한 $P\Rightarrow Q$를 증명해도 그 역인 $Q\Rightarrow P$까지 증명되는 것은 아니다. 두 명제가 동치임을 보이려면 양쪽 방향을 모두 증명해야 한다.

증명된 명제는 정리라고 한다. 다른 정리의 증명에 주로 쓰이는 결과는 보조정리, 이미 얻은 정리에서 곧바로 따라오는 결과는 따름정리라고 부른다. 이러한 명칭의 차이는 결과가 쓰이는 역할에 따른 것으로, 증명에 필요한 논리적 정당화가 서로 다르다는 뜻은 아니다. 참일 것으로 예상되지만 아직 증명되지 않은 명제는 추측이라고 한다.

보편 명제, 존재 명제와 반례

 한정 기호 및 반례 문서를 참고하십시오.

양화사는 어떤 성질이 모든 대상에 성립하는지, 적어도 한 대상에 성립하는지를 나타낸다. 모든 대상에 대한 보편 명제와 어떤 대상의 존재를 주장하는 존재 명제는 증명에서 서로 다르게 다루어진다. 예를 들어 “모든 정수 $n$에 대하여 $n^{2}\geq 0$이다”를 증명하려면 특정한 정수 몇 개가 아니라 임의의 정수에 적용되는 근거가 필요하다. 반면 “$n^{2}=4$를 만족하는 정수 $n$이 존재한다”는 명제에는 $n=2$라는 한 사례가 증명이 된다.

명제가 어떤 대상의 존재와 유일성을 함께 주장한다면 두 조건을 모두 증명해야 한다. 존재를 보이는 것은 조건을 만족하는 대상이 적어도 하나 있음을 뜻하고, 유일성을 보이는 것은 그러한 대상이 둘 이상일 수 없음을 뜻한다. 유일성은 보통 조건을 만족하는 임의의 두 대상이 서로 같음을 보이는 방식으로 증명한다. 예를 들어 $n^{2}=4$를 만족하는 정수는 존재하지만, $2$와 $-2$가 모두 조건을 만족하므로 유일하지 않다.

반례는 보편 명제의 결론을 만족하지 않는 대상이다. “모든 소수는 홀수이다”라는 명제는 짝수인 소수 $2$ 하나로 반박된다. 따라서 보편 명제를 반증하는 데에는 반례 하나로 충분하지만, 그 명제가 성립하는 사례 하나로는 일반적으로 증명할 수 없다. 조건이 붙은 명제의 반례는 가정을 만족하면서 결론은 만족하지 않아야 한다.

역할과 수학적 실천

설명과 발견

증명은 명제의 정당성을 뒷받침하는 동시에, 그 명제가 성립하는 이유와 다른 결과와의 관계를 드러낼 수 있다. 같은 명제의 증명이라도 어떤 성질을 핵심으로 사용하는지에 따라 제공하는 설명은 달라진다. 또한 여러 결과를 공리·정의·정리의 관계로 조직하면, 각각의 결과가 어떤 가정에 의존하는지 파악할 수 있다. 이러한 정당화, 설명, 이론의 체계화는 증명의 서로 연결된 역할이다.

추측을 세울 때에는 수치 계산, 그림, 개별 사례의 관찰과 유추가 단서를 제공한다. 증명을 찾는 과정에서는 이 단서를 검토하면서 필요한 가정이나 보조정리를 발견하기도 한다. 따라서 명제를 발견하는 과정과 증명하는 과정은 상호작용하며, 완성된 증명의 서술 순서가 처음 결과를 발견한 순서와 일치할 필요는 없다.

명제의 증명에서 실제로 사용된 가정을 분석하면 더 일반적인 결과를 얻을 수 있다. 예를 들어 볼록한 연꼴의 네 변의 중점을 차례로 연결하면 직사각형이 된다는 사실을 증명할 때, 중점을 잇는 선분들이 원래 연꼴의 대각선과 평행함을 이용할 수 있다. 이 논증에서는 두 쌍의 이웃한 변의 길이가 같다는 조건보다 대각선이 수직이라는 성질이 핵심이다. 따라서 같은 결론을 대각선이 수직인 모든 볼록 사각형으로 확장할 수 있다.

서술과 검증

일반적인 수학 문헌의 증명은 자연어와 수식, 도형을 함께 사용한다. 이미 알려진 정리는 다시 증명하지 않고 인용하며, 독자가 복원할 수 있는 계산과 추론은 생략하기도 한다. 어느 정도를 자세히 서술하는지는 독자에게 전제하는 지식에 따라 달라진다. 이 때문에 자연어로 서술된 증명의 엄밀성과 모든 추론을 형식 언어로 전개하는 것은 구별된다.

증명의 검증에서는 결론을 이끄는 논증을 재구성하고, 생략된 단계가 실제로 정당화되는지 확인한다. 명시하지 않은 가정이 필요한지, 인용한 정리의 조건이 충족되는지, 각 경우가 빠짐없이 다루어졌는지가 검토 대상이다. 논증의 결함을 발견하면 해당 증명을 보완하거나 수정해야 하지만, 그 사실만으로 증명하려던 명제가 거짓이라는 결론이 나오지는 않는다. 명제의 참·거짓과 제시된 논증의 타당성은 구별되기 때문이다.

증명 방법

증명 방법은 명제의 논리적 형태와 다루는 대상에 따라 달라진다. 직접 증명이나 귀류법은 추론의 전개 방식에 따른 구분이고, 구성적 증명과 비구성적 증명은 존재를 보이는 방식에 따른 구분이다. 조합론적 증명과 확률적 증명은 각각 조합론과 확률론을 활용하는 방법이다. 이러한 구분은 서로 배타적이지 않으며, 하나의 증명에서 여러 방법을 함께 사용할 수 있다.

직접 증명과 대우를 이용한 증명

직접 증명(영어: direct proof)은 가정에서 출발하여 정의와 알려진 결과를 적용함으로써 결론을 얻는다. 예를 들어 “홀수의 제곱은 홀수이다”라는 명제는 홀수의 정의로 증명할 수 있다. 홀수 $n$은 어떤 정수 $k$에 대해 $n=2k+1$로 쓸 수 있으므로

$n^{2}=(2k+1)^{2}=2(2k^{2}+2k)+1$

이다. $2k^{2}+2k$가 정수이므로 $n^{2}$도 홀수이다.

고전 논리에서 함의 $P\Rightarrow Q$는 그 대우인 $\neg Q\Rightarrow \neg P$와 동치이다. 따라서 원래 명제 대신 대우를 증명할 수 있다. 위의 결과는 “정수 $n$의 제곱이 짝수이면 $n$도 짝수이다”라는 명제의 대우이므로, 이 명제의 증명이 되기도 한다.

귀류법

 이 부분의 본문은 귀류법입니다.

귀류법은 결론을 부정하는 가정에서 모순을 이끌어 내는 방법이다. 고전 논리에서는 $\neg P$로부터 모순이 따라오면 $P$를 결론으로 얻는다. 조건 명제 $P\Rightarrow Q$의 경우에는 $P$와 $\neg Q$를 함께 가정한 뒤 모순을 보일 수 있다.

대표적인 예는 ${\sqrt {2}}$가 무리수라는 증명이다. ${\sqrt {2}}$가 유리수라고 가정하면 서로소인 양의 정수 $a,b$에 대해 ${\sqrt {2}}=a/b$로 쓸 수 있다. 그러면 $a^{2}=2b^{2}$이므로 $a^{2}$는 짝수이고, 앞의 결과에 따라 $a$도 짝수이다. $a=2c$를 대입하면 $b^{2}=2c^{2}$이므로 $b$ 역시 짝수이다. 이는 $a,b$가 서로소라는 가정과 모순된다. 따라서 ${\sqrt {2}}$는 무리수이다.

경우를 나누는 증명

가능한 경우를 빠짐없이 나누고 각 경우에서 결론을 보이는 방법도 있다. 예를 들어 정수 $n$에 대해 $n(n+1)$이 짝수임을 보이려면 $n$이 짝수인 경우와 홀수인 경우로 나눌 수 있다. 첫 번째 경우에는 $n$이, 두 번째 경우에는 $n+1$이 짝수이므로 두 경우 모두 곱이 짝수이다. 여기서 검토한 수 자체는 무한히 많지만, 각 수는 두 경우 중 하나에 속하므로 논증은 모든 정수에 적용된다.

수학적 귀납법

 이 부분의 본문은 수학적 귀납법입니다.

홀수의 합 $1+3+\cdots +(2n-1)=n^{2}$의 도해. 한 변에 칸이 $k$개인 정사각형 배열에 $2k+1$개의 칸을 더하면 한 변에 칸이 $k+1$개인 배열이 된다.

수학적 귀납법은 자연수에 따라 주어지는 명제들을 증명하는 방법이다. 모든 양의 정수 $n$에 대해 $P(n)$이 성립함을 보이려면 다음 두 단계를 증명한다.

1. $P(1)$이 성립한다.
2. 임의의 정수 $k\geq 1$에 대해 $P(k)$가 성립한다고 가정하면 $P(k+1)$도 성립한다.

두 번째 단계에서 임시로 두는 $P(k)$를 귀납 가정이라고 한다. 이 두 단계에 의해 첫 명제에서 다음 명제로 계속 나아갈 수 있으므로, 수학적 귀납법의 원리에 따라 모든 양의 정수에 대한 결론을 얻는다. 이는 관찰한 사례로 일반적인 경향을 추정하는 귀납적 추론과 구별되는 연역적 증명이다.

예를 들어 처음 $n$개의 양의 홀수의 합에 대한 등식

$1+3+\cdots +(2n-1)=n^{2}$

은 $n=1$일 때 성립한다. $n=k$에서 성립한다고 가정하면

$1+3+\cdots +(2k-1)+(2k+1)=k^{2}+2k+1=(k+1)^{2}$

이므로 $n=k+1$에서도 성립한다. 따라서 등식은 모든 양의 정수 $n$에 대해 성립한다. 그림에서는 $k^{2}$개의 칸에 새로운 층을 더하는 과정이 이 귀납 단계에 해당한다.

구성적 증명과 비구성적 증명

 직관 논리 문서를 참고하십시오.

어떤 대상의 존재를 보이는 증명에서, 조건을 만족하는 대상을 구체적으로 제시하거나 만드는 방법을 주는 것을 구성적 증명(영어: constructive proof)이라고 한다. 존재를 보이면서도 그러한 대상을 구체적으로 정하지 않는 증명은 비구성적 증명(영어: non-constructive proof)이라고 한다.

예를 들어 “$a^{b}$가 유리수가 되는 양의 무리수 $a,b$가 존재한다”는 명제는 다음과 같이 증명할 수 있다. $c=({\sqrt {2}})^{\sqrt {2}}$라고 하자. $c$가 유리수이면 $a=b={\sqrt {2}}$가 조건을 만족한다. $c$가 무리수이면 $a=c$, $b={\sqrt {2}}$로 두어

$a^{b}=\left(({\sqrt {2}})^{\sqrt {2}}\right)^{\sqrt {2}}=2$

를 얻는다. 어느 경우에도 원하는 두 수가 존재하지만, 이 논증 자체는 $c$가 어느 경우에 속하는지 판정하지 않으므로 비구성적 증명이다.

구성주의 수학에서는 존재와 증명의 의미에 관한 이러한 구별을 논리의 선택에도 반영한다. 예를 들어 직관 논리에서는 임의의 명제에 대한 배중률 $P\lor \neg P$나 이중 부정 제거 $\neg \neg P\Rightarrow P$를 일반적인 원리로 인정하지 않는다. 다만 $P$를 가정하여 모순을 이끌어 내고 $\neg P$를 결론으로 얻는 추론은 직관 논리에서도 허용된다. 이처럼 증명 방법의 정당성은 채택한 논리 체계에 따라 달라진다.

조합론적 증명

 조합론 문서를 참고하십시오.

조합론적 증명(영어: combinatorial proof)에서는 수나 식에 조합론적 의미를 부여하여 등식이나 부등식을 보인다. 등식의 경우에는 같은 대상들을 서로 다른 두 방법으로 세거나, 두 집합 사이에 전단사 함수를 구성할 수 있다.

예를 들어 $n$개의 원소를 가진 집합에서 $k$개의 원소를 고르는 방법의 수인 이항 계수는

${\binom {n}{k}}={\binom {n}{n-k}}\qquad (0\leq k\leq n)$

를 만족한다. $k$개의 원소를 고르는 것은 고르지 않을 $n-k$개의 원소를 정하는 것과 일대일로 대응하기 때문이다. 이 증명은 이항 계수의 계승 공식을 직접 계산하는 대신, 양쪽 식이 세는 대상 사이의 대응을 이용한다.

확률적 증명

 확률론 문서를 참고하십시오.

확률적 증명(영어: probabilistic method)은 확률론을 이용하여 원하는 성질을 가진 대상이 존재함을 보이는 방법이다. 대상을 무작위로 선택했을 때 그 성질이 성립할 확률이 양수임을 보이면, 그 성질을 만족하는 대상이 적어도 하나 존재한다. 여기서 확률은 대상의 선택에 관한 것으로, 증명하려는 명제가 참일 가능성을 추정하는 것이 아니다.

예를 들어 변이 $m$개인 유한 단순 그래프에는 적어도 $m/2$개의 변을 가진 이분 부분 그래프가 존재한다. 각 꼭짓점을 서로 독립적으로, 같은 확률로 두 집합 중 하나에 넣고 서로 다른 집합을 잇는 변만 남긴다. 각 변이 남을 확률은 $1/2$이므로, 남는 변의 수의 기댓값은 $m/2$이다. 모든 분할에서 남는 변의 수가 이 평균보다 작을 수는 없으므로, 적어도 한 분할에서는 $m/2$개 이상의 변이 남는다.

형식적 증명과 컴퓨터

형식적 증명

 형식 체계 및 증명 이론 문서를 참고하십시오.

형식 체계에서는 사용할 기호와 논리식의 구성 방법, 공리와 추론 규칙을 명시한다. 이러한 체계에서의 증명을 형식적 증명(영어: formal proof)이라고 한다. 예를 들어 공리적 증명 체계에서는 전제들의 집합 $\Gamma$로부터 논리식 $\varphi$의 증명을 유한한 논리식의 열

$\varphi _{1},\varphi _{2},\ldots ,\varphi _{n}=\varphi$

로 나타낼 수 있다. 각 $\varphi _{i}$는 다음 중 하나를 만족해야 한다.

1. $\Gamma$에 속하는 전제이다.
2. 해당 체계의 공리이다.
3. 앞에 나온 논리식들로부터 추론 규칙을 적용하여 얻어진다.

이러한 증명이 존재할 때 $\Gamma \vdash \varphi$라고 쓰며, $\varphi$가 $\Gamma$로부터 도출된다고 한다. 예를 들어 전건 긍정은 $P$와 $P\Rightarrow Q$에서 $Q$를 도출하는 추론 규칙이다.

컴퓨터를 이용한 증명과 검증

 자동 정리 증명 및 증명 보조기 문서를 참고하십시오.

컴퓨터는 큰 규모의 계산이나 경우의 검토를 수행하여 증명에 사용될 수 있다. 대표적인 사례가 4색 정리이다. 1976년 케네스 아펠과 볼프강 하켄의 증명은 수학적인 논증과 컴퓨터를 이용한 경우의 검토를 결합하였다. 일반적인 문제를 검토 가능한 유한한 경우들로 환원한 뒤 필요한 검사를 수행한 것으로, 임의로 많은 지도를 색칠해 보는 것과 구별된다.

증명 보조기는 형식적 증명을 작성하는 과정을 지원하고, 그 증명이 정해진 논리 체계의 규칙을 따르는지 검사하는 프로그램이다. 4색 정리에는 Coq를 이용하여 2005년에 완성된 형식적 증명도 있다. 이 작업에서는 계산 프로그램의 실행뿐 아니라, 계산이 올바른 결과를 내는 이유와 그 결과가 정리의 결론으로 이어지는 논증도 형식화하였다. 기계 검증의 대상은 입력된 형식적 명제와 그 증명이므로, 형식화한 명제가 원래 의도한 수학적 내용을 표현하는지도 확인해야 한다.

자동 정리 증명은 프로그램이 증명에 필요한 추론을 탐색하는 분야이다. 증명을 찾아내는 작업과 주어진 증명이 올바른지 검사하는 작업은 서로 다르다. 실제 증명 보조기에는 자동화 기능이 포함될 수 있으므로, 사람이 증명의 주요 단계를 정하고 일부 계산이나 세부 추론을 프로그램에 맡기는 방식으로 두 작업을 결합하기도 한다.

증명 가능성과 공리

증명과 참의 구별

 건전성 및 괴델의 완전성 정리 문서를 참고하십시오.

수리논리학에서는 형식적으로 증명할 수 있다는 것과 주어진 해석에서 참이라는 것을 구별한다. 자유 변수가 없는 문장들의 집합 $\Gamma$와 문장 $\varphi$에 대해, $\Gamma \vdash \varphi$가 기호와 추론 규칙에 따른 도출을 뜻하는 데 비해, $\Gamma \models \varphi$는 $\Gamma$의 모든 명제가 참인 모든 구조에서 $\varphi$도 참이라는 뜻이다. 전자는 증명의 형식에 관한 것이고, 후자는 논리식의 해석에 관한 것이다.

증명 체계의 건전성은 $\Gamma \vdash \varphi$이면 $\Gamma \models \varphi$임을 뜻한다. 괴델의 완전성 정리는 고전적인 1차 논리에서 적절한 증명 체계를 사용하면 그 역도 성립함을 보인다. 이때 완전성은 전제가 참인 모든 구조에서 성립하는 명제를 증명할 수 있다는 뜻이며, 특정한 공리계에서 모든 명제의 참과 거짓이 결정된다는 뜻은 아니다.

독립성과 불완전성

 이 부분의 본문은 괴델의 불완전성 정리입니다.

 연속체 가설 문서를 참고하십시오.

어떤 명제 $\varphi$와 그 부정 $\neg \varphi$가 모두 주어진 공리계 $T$에서 증명되지 않으면, 그 명제는 $T$로부터 독립이라고 한다. 독립성은 그 명제와 특정한 공리계 사이의 관계이다. 따라서 어떤 명제가 독립임을 보이는 것은 지금까지 증명을 찾지 못했다는 진술보다 강한 결과이다.

제1 불완전성 정리의 로서에 의한 강화에 따르면, 무모순이고 공리들을 알고리즘으로 열거할 수 있으며 로빈슨 산술(영어: Robinson arithmetic)을 포함하는 고전 1차 논리의 형식 이론에는 그 이론에서 증명도 반증도 할 수 없는 문장이 존재한다. 로빈슨 산술은 자연수의 덧셈과 곱셈에 관한 기본적인 성질을 표현하는 이론이다. 이 결과는 모든 공리계에 무조건 적용되는 것이 아니라, 이러한 효과적 공리화와 산술적 표현 능력 등의 조건 아래에서 성립한다.

연속체 가설은 주어진 공리계에서 독립인 명제의 대표적인 예이다. 자연수 집합보다 크고 실수 집합보다 작은 크기를 가진 집합은 없다는 명제로, 체르멜로-프렝켈 집합론에 선택 공리를 더한 ZFC가 무모순이라면 ZFC에서는 연속체 가설도 그 부정도 증명할 수 없다. 이는 쿠르트 괴델과 폴 코언의 결과를 합쳐 얻어진다. 이 독립성은 ZFC의 증명 능력에 관한 결과이며, 명제가 참도 거짓도 아니라는 결론과는 구별된다.

역사

 수학사, 에우클레이데스의 원론 및 수학기초론 문서를 참고하십시오.

고대와 중세의 증명

고대 그리스의 유클리드가 저술한 《원론》은 정의와 공준, 공통 개념에서 출발하여 명제들을 차례로 증명하는 체계적인 구성을 갖추고 있다. 제1권의 첫 명제는 주어진 선분을 한 변으로 하는 정삼각형의 작도이며, 원의 정의와 길이의 같음에 관한 원리를 이용하여 구성된 삼각형의 세 변이 같음을 보인다. 다만 《원론》의 논증이 현대적인 형식 체계와 같은 것은 아니다. 예를 들어 첫 명제에서는 두 원의 교점이 존재함을 사용하지만, 이를 보장하는 가정을 별도로 명시하지 않는다.

고대 중국에서는 알고리즘이 올바른 결과를 내는 이유를 밝히는 논증이 발달하였다. 유휘가 263년에 완성한 《구장산술》의 주석에는 계산 절차를 단계별로 분석하고, 연산 사이의 관계를 이용하여 그 절차를 정당화하는 증명이 담겨 있다. 이러한 논증은 문제의 답을 계산하는 방법과 그 방법이 성립하는 이유를 함께 다룬다.

중세 이슬람 수학에서는 대수학의 계산 절차를 기하학적 논증으로 정당화하기도 하였다. 9세기의 알콰리즈미는 이차방정식의 풀이를 도형의 넓이와 연결하였다. 예를 들어 현대 기호로 $x^{2}+10x=39$라고 쓰는 문제를 정사각형을 완성하는 작도로 바꾸어, $(x+5)^{2}=64$에서 양의 해 $x=3$을 얻었다. 도형에 대한 논증은 해당 계산이 성립하는 이유도 제시하였다.

엄밀화와 공리화

근대 미적분학의 발전은 무한 과정에 대한 논증을 어떻게 정당화할 것인지라는 문제를 제기하였다. 19세기에는 코시와 바이어슈트라스 등의 연구를 통해 극한과 수렴을 다루는 정의와 증명이 정교해졌다. 이 과정에서 함수나 무한급수에 관한 직관을 그대로 적용하기보다, 계산과 추론이 성립하는 조건을 명확히 구별하게 되었다.

평행선 공준을 다른 공준들로부터 증명하려는 연구는 비유클리드 기하학의 발전과 연결되었다. 평행선 공준을 부정하여 얻은 결과가 익숙한 공간 직관과 다르다는 사실이 곧 논리적 모순을 뜻하지는 않았다. 이러한 전개는 어떤 결론이 선택한 공리들에 의존하는지를 분석하는 공리적 관점을 강화하였다.

19세기 말부터 20세기 초에는 집합론과 수리논리학의 발전을 바탕으로 수학의 언어와 추론 자체를 명확히 하려는 연구가 이루어졌다. 다비트 힐베르트는 수학을 형식적인 체계로 나타내고 증명 자체를 수학적 연구 대상으로 삼아 그 체계의 무모순성을 밝히려 하였다. 이러한 연구에서 현대의 증명 이론이 발전하였으며, 1931년에 발표된 괴델의 불완전성 정리는 일정한 조건을 갖춘 형식 이론의 증명 능력에 제약이 있음을 밝혔다.

같이 보기

• 논증
• 수리철학
• 영지식 증명
• 증명 이론
• 자동 정리 증명

참고문헌

• Bridges, Douglas; Palmgren, Erik; Ishihara, Hajime. “Constructive Mathematics” (영어). 《Stanford Encyclopedia of Philosophy》. 2026년 9월 27일에 확인함. 
• de Villiers, Michael (1990). “The Role and Function of Proof in Mathematics” (PDF) (영어). 《Pythagoras》 (24): 17–24. 
• Euclid. “Euclid’s Elements, Book I” (영어). David E. Joyce 편집·해설. 《Clark University》. 2026년 9월 27일에 확인함. 
• Gonthier, Georges (2008). “Formal Proof—The Four-Color Theorem” (PDF) (영어). 《Notices of the American Mathematical Society》 55 (11): 1382–1393. 
• Hammack, Richard (2018). 《Book of Proof》 (PDF) 3판 (영어). Richmond, Virginia: Richard Hammack.  제3.4판 공개 PDF.
• Gila Hanna; Michael de Villiers 편집 (2012). 《Proof and Proving in Mathematics Education: The 19th ICMI Study》 (PDF) (영어). New ICMI Study Series 15. Dordrecht: Springer. doi:10.1007/978-94-007-2129-6. ISBN 978-94-007-2128-9. 
• Joyce, David E. “Euclid’s Elements, Book I, Proposition 1” (영어). 《Clark University》. 2026년 9월 27일에 확인함. 
• Koellner, Peter. “The Continuum Hypothesis” (영어). 《Stanford Encyclopedia of Philosophy》. 2026년 9월 27일에 확인함. 
• Open Logic Project. “First-order Logic” (PDF) (영어). 2026년 9월 27일에 확인함.  2026년 7월 12일 개정본.
• Portoraro, Frederic. “Automated Reasoning” (영어). 《Stanford Encyclopedia of Philosophy》. 2026년 9월 27일에 확인함. 
• Raatikainen, Panu. “Gödel’s Incompleteness Theorems” (영어). 《Stanford Encyclopedia of Philosophy》. 2026년 9월 27일에 확인함. 
• Rathjen, Michael; Sieg, Wilfried. “Proof Theory” (영어). 《Stanford Encyclopedia of Philosophy》. 2026년 9월 27일에 확인함. 
• Thurston, William P. (1994). “On Proof and Progress in Mathematics” (영어). 《Bulletin of the American Mathematical Society》 30 (2): 161–177. doi:10.1090/S0273-0979-1994-00502-6.  각주의 공개 원고 쪽수는 이 PDF의 쪽수를 따른다.
• Zhao, Yufei; Lin, Andrew (2019). “The Probabilistic Method in Combinatorics” (PDF) (영어). 《MIT 18.218 강의노트》. 2026년 9월 27일에 확인함.  Zhao 강의, Lin 정리.