코딩, 전산과 순수 수학은 어떻게 관계가 있는가? 어떻게 도울 수 있는가?

무한에 대해서 우선 이야기를 해보자.

 

 조지 가모프의 책 "1,2,3 그리고 무한"에 보면 칸토어의 무한을 설명하기 위해 3까지 밖에 세지 못하는 아프리카 호텐토트 부족의 이야기를 한다. 그러면 이 부족은 5와 10이 어떻게 다른지 세지 않고 알 수 있는가? 이는 "유한의 수를 세는 방법으로 무한을 다룰 수 없는데 어떻게 하지?" 라는 질문의 더 단순화된 버전이다.

 

 결론부터 이야기하면, 정답은 논리를 세워 비교하는 것이다. 기존의 숫자를 세어가는 형태의 단순 수학 기법에서, 그 숫자없이 두 그룹의 크기를 어떤 논리 체계로 세는 방법을 만들면 된다. 그리고 칸토어가 제시한 방법은 일대일 대응을 통해 이러한 체계를 만드는 것이다.

 

 그래서 자연수와 홀수와 짝수는 간단한 방법으로 빠짐없이 상호 대응시키는 방법을 찾아주면, 그 둘이 같다는 것을 증명할 수 있다. 무한이라는 셀 수 없는 수의 개념에 이렇게 세는 것과 유사한 효과가 나도록 논리적인 방법을 만든 것이다. 그래서 이것을 "논리로 센다"라고 표현할 수도 있다.

 

 마찬가지로 호텐토트 부족도 두 그룹의 원소를 하나하나 대응시켜 가면 남는 것이 있는 그룹이 더 많다는 것을 알 수 있다. 물론 정확히 수를 셀 수는 없었겠지만 최소한 많거나 적거나, 같다는 것을 알 수 있다. 그리고 칸토어의 논리에 따라, 앞서 이야기한 자연수나 홀수나 짝수는 사실 무한의 수 체계에서는 이름만 다른 같은 존재이다. 논리적으로는 다를 것이 없는 같은 무한 체계이다. 둘을 동일하게 서로 빈틈없이 짝지을 수 있기 때문이다.

 

          자연수) 1,2,3,4,5,6,7,...

          짝__수) 2,4,6,8,10,12,14...

          홀__수) 1,3,5,7,9,11,13... 

 

[자연수와 짝수, 홀수는 위와 같이 증가시켜 자연수에 1:1로 빈틈없이 대응시킬 수 있다]

 

 가만히 보면 이렇게 수학이란 기계화 할 수 있는, 즉 코딩화 할 수 있는 논리체계의 조합이다. 어떤 논리 체계를 세우고 그 논리를 조합해 가는 방식이다. 마치 컴퓨터 코딩이 어떤 절차를 지니고, 함수를 만들어서, 그 절차대로 진행시키는 것과 다르지 않다.

 

 이런 방식에서 수학적 증명의 일부는 이렇게 코딩으로 간접적으로 나타낼 수 있다. 이를테면 골드바흐의 추측을 예로 들어보자. 골드바흐의 추측을 검사하는 코드는 아래와 같다.

 

  for(int i=2;i<MAX;i=i+2) {

     if(checksumofprime(i)==false) {

          print("exception case\n");

  }

 

#checksumofprime은 i가 두 소수의 합인지 아닌지 검사

boolean checksumofprime(int n) {

     ....

}

 

 이 코드의 MAX가 무한대일때 위 코드가 exception이 출력이 되지 않는다면 골드바흐의 추측이 증명된다. 그리고 checksumofprime은 또 다른 코드의 조합으로 내려가서 만약에 특정 함수가 무한에 대해서 일관성을 지닌다면 그것은 증명이 끝난 것이고 나머지 함수들이 모두 증명이 되면 전체 증명이 끝나게 된다.

 

 만약에 제시한대로 상기 코드를 설계했을때 기계가 자동으로 어떤 형식체계로 그것이 무한일때 참인지 아닌지 판별할 수 있다면(모든 경우에 판별되지는 않겠지만) 상기 증명이 성립되게 된다.

 

 그런 면에서 수학은 여러 함수들을 가지고 순차적으로 실행해서 어떤 작동을 하는 프로그램을 닮았다. 그리고 그 특성도 비슷한데 이 논리들이 서로 다른 관점에서 "간결한 형태의 수정이 가능"하다면 무한대의 작동을 하지 않고도 옳바른지 알아낼 수 있다. 그런데 간결하게 또다른 논리체계로 바라보기 어렵다면 이제 증명이 쉽지 않게 된다. 이 경우는 다시 함수들을 더 분해하고, 증명된 함수들의 조합으로 설명해내야 하기 때문이다. (여기서 간결하게 수정이 가능하다는 것은 마치 '소수'라는 필터가 복잡한 절차를 거치지만, n번째 소수가 어떤 손쉬운 방법에 의해서 도출될 수 있는 것과 같은 변환 과정이다.)

 

 예를 들면 페르마의 정리를 보자. x^n + y^n = z^n을 만족하는 n이 2가 초과되는 x,y,z 정수 쌍이 없다는 증명이다.

역시 이 계산도 x,y,z,n을 각기 자연수 범위에서 모두 대입하여 조사하는 코드를 작성할 수 있다. 그러나 그 코드를 다른 논리체계로 변환하여 단순화하기가 매우 어렵다. 이 부분은 이제 인류의 노하우 영역으로 진입하게 된다. 칸토어가 무한의 체계를 1:1 대응 논리로 풀어냈듯이, 페르마의 정리를 위한 단순한 체계가 존재할까? 쉽게 찾을 수 없었기 때문에 이 체계에 대한 도출은 이제 길고 긴 시행착오가 된다. 수많은 함수들이 이 과정에서 사용될텐데, 전체를 관통하는 논리체계를 만들기 어려우니까 각 함수별로 분할하여 혹은 특정 함수는 더 세분화하여 각각을 증명해야 하기 때문이다. 일례로 n=2일때, n=3일때 식으로 차례대로 일부가 증명되어 나가는 과정도 유사하다.

 

 그러면에서 이런 식의 수학적 증명의 어떤 부분은 대형 SI 사업을 닮았다. 수많은 함수들과 세부 증명으로 분할하여 프로젝트를 다수의 인원이 오래 진행해야 하는 것이다. 그리고 그것이 최적화 되는 경우도 있지만 그렇지 않은 경우도 많다(결과적으로 복잡하고 긴 증명이 된다)

 

 나중이 되면 상기 코드의 점검을 다른 논리틀 하에서 컴퓨터가 자동 증명해주는 체계를 만들 수는 없을까? 특정 코드 유형에만 제약을 가해도 좋다. 아니면 몇가지 절차를 거쳐서 해도 좋다. 소수(prime number)에 대한 여러가지 규칙을 찾아내는 과정도 이러한 방향과 동일할 수 있다고 생각한다. 소수를 숫자의 원소라고 하지만, 코딩상에서는 1과 자기 자신외에는 나누어지지 않는 수라는 태깅 정도의 검사로 바라볼 수 있다. 이러한 명확한 정해진 검사절차를 어떻게 다른 시야에서 보고 그 코딩의 경계까지 모두 아우르는 다른 논리 해석을 자동으로 만들 수 있을까? 골드바흐의 추측이 4개의 소수의 합 정도라는 것 까지 증명된 것은 역시 이 골드바흐 추측 코드의 군데군데를 다시 세분화하고, 어느 정도의 것들은 기존의 증명된 논리(즉 함수)를 가지고 만들어 낸게 아닌가?

 

이미 형식체계의 불완전성이나 코드의 정상유무를 완전히 밝히는 것이 불가능하다는 것은 증명되었으나, 이러한 코드화 가능한 절차를 분할하고 개별로 증명하여 전체를 자동증명 어떤 시도가 있었던 것은 아니다. 혹은 기존의 증명을 통해 어떤 코드 들의 검사가 n이 무한일때 모두 완전하다고 하면 해당 코드의 조합으로 만드는 모든 것은 증명이 완료된 것이 아닌가? AI가 다양하게 사용되는 이때에 이런 종류의 수학과의 협업이 가능하지 않을까 상상해본다.