Proof Assistants at the interplay of mathematical cultures: a semiotic-cultural analysis of proof in higher education

대학 수학의 세계에서 증명이라는 행위는 단순히 문제를 푸는 것 그 이상이며, 하나의 문화적 관습이다. 그것은 학생들이 고등학교에서 고등 교육으로 넘어갈 때 반드시 배워야 하는 특정한 사고방식, 글쓰기, 그리고 아이디어를 검증하는 방식이다. 수십 년 동안 교육자들은 학생들이 초기에 배웠던 직관적이고 비형식적인 논증과 대학 수준에서 요구되는 엄격하고 명시적인 표준 사이의 간극을 메우기 위해 고군투쟁하는 모습을 지켜봐 왔다. 최근 이 풍경에 새로운 도구가 등장했다. 바로 증명 보조기(proof assistant)다. 이 프로그램들은 수학적 논증을 절대적인 정밀도로 점검하도록 설계되었으며, 작성자가 단 하나의 단계도 설명 없이 남겨두지 못하도록 강제한다. 어떤 이들은 이 도구들이 수학을 더욱 엄격하게 만드는 방법이라고 보는 반면, 다른 이들은 이것이 창의성을 억누르거나 이미 어려움을 겪고 있는 학생들을 혼란스럽게 할 수 있다고 우려한다. 문제는 단순히 이 프로그램들이 도움이 되느냐 방해가 되느냐가 아니라, 증명이 쓰이고 이해되는 본질적인 방식을 어떻게 변화시키느냐 하는 것이다.

두 곳의 프랑스 대학교에 속한 연구팀은 이러한 상호작용을 면밀히 조사하기로 했다. 그들은 단순히 학생들이 더 잘 배우는지만을 묻지 않았다. 대신 컴퓨터 프로그램이 학생들의 사고 과정을 어떻게 재형성하는지를 관찰했다. 연구는 학생들이 '버보스 린(Verbose Lean)'이라 불리는 특정 유형의 증명 보조기를 사용하는 1학년 수업에 초점을 맞추었다. 일반적인 프로그래밍 언어가 코드처럼 보이는 것과 달리, 버보스 린은 학생들이 통제된 형태의 자연어를 사용할 수 있게 하여 수학자들이 종이 위에 쓰고 말하는 방식에 더 가깝게 느껴지도록 한다. 연구진은 한 쌍의 학생들이 고전적인 문제, 즉 수열이 양수 값에 점점 가까워진다면 그 수열의 항들은 결국 양수가 되어야 한다는 것을 증명하는 과정을 관찰했다. 연구진은 학생들의 대화, 종이 위의 낙서, 화면에 타이핑하는 내용, 그리고 컴퓨터의 피드백을 기록함으로써, 수학적 아이디어가 거친 생각에서 컴퓨터에 의해 검증된 사실으로 이동하는 과정을 상세히 지도화했다.

연구진이 발견한 것은 컴퓨터가 단순히 최종 답안을 확인하는 것이 아니라, 학생들이 보통 당연하게 여기는 숨겨진 가정들을 드러내는 거울 역할을 한다는 점이었다. 일반적인 수학 수업에서 학생은 작은 세부 사항을 건너뛰거나 어떤 단계가 당연하다는 '느낌'에 의존할 수 있다. 그러나 컴퓨터는 모든 개체, 모든 조건, 그리고 모든 논리적 도약을 명시적으로 이름 붙이고 정당화할 것을 요구한다. 이 연구는 이러한 요구가 일종의 문화적 변화를 강요한다는 것을 보여주었다. 학생들은 자신의 유동적이고 직관적인 아이디어를 기계가 이해할 수 있는 엄격한 구조로 번역해야 했다. 이 과정은 매끄럽지 않았다. 그것은 학생들의 종이 메모, 구두 표현, 컴퓨터의 오류 메시지, 그리고 교사의 설명 사이의 끊임없는 상호작용을 포함했다.

연구진은 학생들의 작업 전반에 나타난 특정 수학적 표현을 추적했다. 처음에 학생들은 이 표현을 추론에 도움이 되는 숫자로 취급했다. 그러나 학생들이 이를 컴퓨터에 입력하려고 했을 때, 프로그램은 이를 거부했다. 컴퓨터는 그 숫자가 수학적으로 틀렸다고 말한 것이 아니라, 위치가 잘못되었다고 말했다. 학생들은 이를 수열의 위치를 나타내는 라벨로 사용하려 했으나, 컴퓨터는 그 역할에 정수를 필요로 했던 반면 그들의 표현은 분수였다. 이 순간은 전환점이 되었다. 이는 증명 보조기의 세계에서는 숫자가 수행하는 역할이 숫자 그 자체만큼 중요하다는 것을 깨닫게 했다. 학생들은 전략을 재고하여, 해당 표현을 자신의 논증 중 다른 부분으로 옮겨야 했고, 그곳에서 마침내 컴퓨터의 엄격한 규칙에 부합하게 되었다.

이 투쟁은 컴퓨터 혼자만의 힘으로 해결되지 않았다. 같은 교실에서 칠판 앞에 서 있던 교사는 개념을 시각적으로 설명하기 위해 도표를 그렸다. 그는 학생들이 왜 자신들의 숫자가 목표값보다 작아야 하는지를 이해할 수 있도록 돕는 '크기'를 가진 '창(window)'을 묘사했다. 이 시각적 설명은 컴퓨터의 첫 번째 시도 거부와 결합되어 학생들이 생각을 재구성하는 데 도움을 주었다. 그들은 결국 자신들이 씨름하던 숫자가 수열의 위치가 아니라, 측정해야 할 간격의 크기라는 것을 깨달았다. 이 전환을 마쳤을 때, 컴퓨터는 그들의 논증을 수용했다. 최종 증명은 아이디어에서 해결책으로 가는 직선이 아니었다. 그것은 하나의 기호가 말해지거나, 종이에 쓰이거나, 교사에 의해 설명되거나, 혹은 기계에 의해 검증되느냐에 따라 그 의미가 변하는 복잡한 여정이었다.

이 연구는 증명 보조기가 저자들이 '인식적 폭로자(epistemic revelators)'라고 부르는 도구, 즉 보이지 않는 것을 보이게 만드는 도구 역할을 한다고 제안한다. 이들은 전문가와 학생들이 보통 당연하다고 여겨 말하지 않는 수학의 '생략된 생각들(unthoughts)'을 드러낸다. 전통적인 교실에서 이러한 간극은 눈에 띄지 않을 수 있다. 그러나 증명 보조기가 있는 교실에서 컴퓨터는 학생이 모든 간극을 채우도록 강요하며, 수학적 타당성을 규정하는 숨겨진 규칙들을 노출시킨다. 연구진은 이것이 컴퓨터가 인간보다 낫다거나 인간이 컴퓨터보다 낫다는 의미가 아니라고 주장한다. 대신, 두 체계가 협력하여 서로 다른 방식의 증명 사고가 충돌하고 융합되는 새로운 공간을 만들어낸다는 것이다.

연구 결과는 이러한 도구의 도입이 고등 교육의 증명 문화를 변화시킨다는 것을 나타낸다. 이는 단순히 기술적 엄격함을 한 층 더하는 것이 아니라, 무엇이 옳다는 것의 의미를 학생들이 어떻게 이해하는지를 재구성하는 일이다. 연구는 학생들이 단순히 코드를 작성하는 법을 배우는 것이 아니라, 서로 다른 의미의 세계 사이를 항해하는 법을 배운다는 것을 보여준다. 학생들은 자신의 직관적 이해를 기계가 검증할 수 있는 언어로 번료하는 동시에, 교사의 인간적인 설명에도 귀를 기울여야 한다. 컴퓨터의 오류 메시지는 단순한 장애물이 아니라, 학생의 이해가 어디에서 불완전한지를 알려주는 신호이다. 학생들에게 암묵적인 가정을 명시적으로 만들도록 강요함으로써, 이 도구들은 수학적 지식이 어떻게 구축되고 검증되는지를 연구할 수 있는 독특한 기회를 제공한다.

궁극적으로, 이 논문은 증명 보조기가 중립적인 도구가 아니라고 결론짓는다. 이 도구들은 무엇이 유효한 논증인지에 대한 특정한 관념을 내포하고 있다. 학생들이 이를 사용할 때, 그들은 단순히 수학을 배우는 것이 아니라 사고하고 소통하는 새로운 문화적 규칙을 배우는 것이다. 연구진은 이러한 변화가 증명이 어떻게 가르쳐지는지, 전문가들에 의해 어떻게 실행되는지, 그리고 기계에 의해 어떻게 검증되는지 사이의 연속성과 단절을 연구할 수 있는 특권적인 장소를 제공한다고 제안한다. 초기 혼란에서 최종적인 성공에 이르기까지 연구에 참여한 학생들의 여정은, 컴퓨터와 함께 증명하는 법을 배우는 것이 하나의 번역 과정임을 보여준다. 그것은 수학적 아이디어의 의미가 인간의 직관, 교사의 지도, 그리고 기계의 정밀함 사이의 상호작용을 통해 테스트되고, 재형성되며, 궁극적으로 안정화되는 과정이다.