아, 이건 아프다. 개인적인 일화 겸 푸념을 하자면, 내가 수학/컴퓨터과학이 아니라 소프트웨어 엔지니어링을 하게 된 이유 중 하나는 교실에서 구두로 접할 때와 혼자 책으로 볼 때의 수학 이해력 차이가 너무 컸기 때문임
나는 글로 쓰인 정리를 이해하는 데 비정상적으로 많은 시간이 필요하고, 결국 알고 보면 쉬운 내용이 내 취향에는 형편없이 설명되어 있었다는 느낌이라 매우 불만족스러움
다만 내 진단은 조금 다름. 세부 사항이 부족해서가 아니라, 오히려 동기와 개요가 부족한 게 문제라고 봄. 증명은 모두 정확히 거꾸로 쓰인 것처럼 보임. 문제를 오래 고민해 증명을 찾아낸 뒤, 그 사고 과정을 지우고 마지막 단계부터 증명을 쓰기 시작함
예를 들어 증명은 보통 “ɛ = n^2 / 36을 택하자”로 시작해서, 왜 그 엡실론이 기계적으로 필요한지 한 번 읽어야 하고, 그 기술적 장치 뒤의 아이디어를 이해하려고 또 고민해야 하며, 그 아이디어로 머릿속에서 비형식 증명을 해본 다음, 마지막으로 그 아이디어를 염두에 두고 증명이 올바른 형식화인지 다시 읽어야 함. 형식화는 유용하지만, 이해 그 자체는 아님
Reed-Solomon도 예시가 됨. Wiki는 “N차 다항식은 N+1개 점에서 보간 가능하다. K개 점을 중복 전송하면 일부를 잃어도 계수를 복구할 수 있다”고 말할 수 있었는데, 대신 장황한 난해한 설명이 이어짐 (previously)
최근 예로는 Tao의 Analysis 정리 1.5.8, 즉 콤팩트 집합에서는 모든 열린 덮개가 유한 부분덮개를 갖는다는 내용이 있음. 곧바로 “y를 택하고, V_a를 택하고, 공이 있고, 반지름 r이 있고…”로 들어가는데 틀린 말은 아니지만 왜 그렇게 하는지 알기 어려움
형식을 흡수하고 나서야 핵심 아이디어가 보임. 유한 부분덮개가 필요하니 “가장 큰” 집합을 탐욕적으로 고르는 게 자연스럽지만, 가장 크다는 게 무슨 뜻인지 정해야 함. 한 점을 고정하면 그 점에 상대적으로 가장 큰 집합을 고를 수 있고, 공을 키우다 덮개의 원소가 하나만 남게 만들면 됨. 공들이 무한히 작을 수는 없고, 그러면 콤팩트성을 써서 반지름 0인 공을 가진 점을 뽑게 됨. 따라서 공은 최소 ɛ만큼 넓고, 아직 덮이지 않은 점에 대해 가장 큰 집합을 계속 고르면 됨. 유한 단계에서 끝나면 성공이고, 끝나지 않으면 서로 ɛ만큼 떨어진 점들의 수열이 생겨 콤팩트성과 모순됨
핵심 아이디어는 항상 형식화보다 훨씬 단순하고, 일단 그걸 잡으면 부등식을 충분히 다듬으면 어떤 형식화는 당연히 성립할 것처럼 보임. 형식화는 여전히 필요함. 실수로 선택공리 같은 것에 의존했는지 모를 수 있으니까. 하지만 아이디어를 전달하는 수단으로는 형편없음. 마치 퀵 정렬을 어셈블리 코드에서 역추적하는 것 같음
수학을 제시하는 올바른 방식은 정리를 출발점이 아니라 결과로 두고, “어떻게 이걸 발견할 수 있었는가” 모드로 설명하는 것이라고 봄
물론 가끔은 “정말로 이게 증명한다는 걸 납득할 때까지 붙잡고 흔드는” 논증도 있다는 걸 부정하지는 않지만, 내가 접한 비교적 순한 수학 안에서는 그런 경우가 드문 편임
이 댓글을 보니 케이크 굽기가 떠오름
교과서의 정리는 요리책에 실린 완성된 케이크 사진 같고, 증명은 레시피 같음. 케이크를 만들면서 생기는 난장판은 실제로 잘 보이지 않음
빠진 것은 같은 케이크를 구우려면 여전히 제빵에 대한 이해와 기술이 필요하다는 점임. 레시피에는 반죽의 농도나 잘못됐을 때 어떻게 고칠지 같은 내용이 빠질 수 있음. 또한 제빵의 “제1원리”를 안다고 바로 제빵사가 되는 것도 아님. 기본 아이디어는 있어도 그것들을 조합해 케이크를 구워야 함
수학도 다른 현대 학문과 같다고 봄. 진열장에는 케이크가 가득하고, 최고의 제빵사들은 더 많은 케이크를 굽도록 연구비를 받음. 스스로 제빵사가 되려면 빵집에서 견습하며 요령을 배우고, 상사의 레시피만 쓰는 대신 자기 케이크를 굽기 시작해야 함. 여기에는 시간과 노력, 약간의 운이 필요함
BetterExplained의 Kalid Azad가 “Developing Your Intuition For Math”에서 이걸 꽤 잘 요약했음 https://betterexplained.com/articles/…
DNA 서열은 고양이에 대한 매우 정밀한 설명일 수 있지만, 그것만 보고 그 동물을 머릿속에 그릴 수는 없음
참고로 Reed-Solomon에서 “과잉 표본화” 방식은 실제로 쓰이지 않는다는 점도 일부 문제임. 대신 메시지를 다항식의 계수로 두고, 전체 다항식이 0을 제외한 모든 점에서 0이 되도록 계수를 몇 개 더 추가함
이렇게 포맷하면 검사와 정정이 더 효율적이고, 이를 R-S의 BCH 관점이라고 부름. 다만 BCH는 코드의 한 부류 전체이기도 함
그래도 구현하면서 이 내용을 정말 많이 읽어본 뒤에도 R-S와 BCH에 대한 Wikipedia 문서는 대체로 이해 불가능하다는 데 동의함. 멋진 리터레이트 프로그래밍 방식의 gf256 라이브러리, 특히 gf256::rs가 없었다면 진전이 없었을 것 같음
학부 수준에서 수학을 공부한 사람으로서 공감함. 많은 증명은 뒤돌아보면 말이 되지만, 처음 보일 때는 “어떻게 저기에 도달했지?”라는 생각이 자주 듦
다만 경험상 어떤 정리는 다른 정리보다 증명하기 쉬움. Algebra I 수업에서는 시험 중 하나가 교수가 즉석에서 고른 임의의 정리를 증명하는 것이었음. 위협적으로 보일 수 있지만, 이미 증명된 것들을 오래 증명하다 보면 패턴이 보이기 시작함. 게다가 다른 증명에 쓰이는 정리도 더 많이 외우게 됨
쉽다는 말은 아니지만, 그 수준에서 수학을 공부하면 머릿속에서 무언가가 열려 가능해지는 느낌이 있음. 형식화가 과해 보일 수는 있어도, 수학자가 다른 사람들이 보지 못하는 결론에 도달할 수 있게 해주는 것이기도 함
물리과학 쪽 개인 경험으로는, 많은 부분이 학술 논문이 쓰이고 출판되고 평가되는 방식에서 온다고 봄
논문 작성과 출판 과정은 실제로 과학을 설명하도록 유도하지 않고, 세부 사항에 시간을 너무 “낭비”하지 않으면서 그럴듯하고 약간 설득력 있어 보이는 말을 하도록 유도함. 증명에서 보이는 이런 편향도 매우 비슷해 보임
출판사를 과학에서 빼야 함
“시간을 너무 낭비하지 않으면서” 정도가 아니라 더 나쁨
“이걸 어떻게 찾았는가”를 설명하려면 완전히 정당화되지도, 정밀하지도 않은 모호하고 거친 진술을 해야 함. 심사자들은, 그 장소가 자체 출판이지만 색인되는 학회 프로시딩이나 오버레이 저널이어도, 어느 정도 거짓인 문장이 최종 채택본에 남는 것을 꺼림
그래서 첫 제출본에 직관적 설명이 있었더라도 결국 빠지는 일이 생김
더 나쁜 경우도 있음. 서론을 잘 쓰고 논문을 채택되기 좋게 최적화하는 데 능한 내 공저자는, 명제 버전을 고를 때 보통 트레이드오프가 있다고 설명하곤 함. 가장 채택되기 쉬운 버전이 그 논문을 좋아하고 인용할 사람들에게는 최악인 경우가 많음. 모든 버전이 참이고 같은 수준의 증명 품질로 증명될 수 있어도 그렇다
동의함. 제한적인 이론 컴퓨터과학 경험으로 보면, 학회 페이지 제한 때문에 전체 증명이 본문에서 빠져 보통 철저히 심사되지 않거나 때로는 비공식적으로만 공개되는 부록으로 밀려나는 일이 많음
그래서 인센티브가 맞지 않음. 다만 이번에는 출판사 잘못이라기보다, 학자들이 실제로 해야 할 작업이 아니라 출판 지표만으로 보상받는 구조 때문일 수 있음
교과서에 대해서는 글의 주장에 꼭 동의하지 않음. 좋은 생략은 증명을 더 읽기 쉽게 만들고 독자가 생각하도록 유도할 수도 있음. 최악의 경우 다른 교과서나 원전을 보면 됨. 하지만 연구 논문에서 불완전한 증명을 만나면 매우 짜증날 수 있음. 여기서는 누가 정말 전체 증명을 가지고 있는지 의심이 스며들고, 정신 차려보면 일주일/한 달/일 년이 지나 있을 수 있음
수학 대학원생으로서 이 문제에는 양면이 있다고 봄. 때로는 제시된 증명이 꽤 높은 수준이라 특정 단계를 정말 모르겠을 때 짜증나지만, 반대로 빈칸을 채우는 과정이 모든 걸 다 받는 것보다 실력 향상에 더 유용할 때가 있음
증명이 명제 1에서 명제 2로 넘어가는데 바로 이해되지 않으면, 첫째로 저자와 더 나아가 해당 분야의 수학 공동체가 무엇을 자명하다고 여기는지에 대한 직관을 줌. 이는 어떤 결과를 직관적으로 깊이 익혀야 하는지 알려주기 때문에 가치 있음
둘째로 중간 단계를 채워 넣고 논증이 탄탄하다고 스스로 납득하면, 그 중간 단계를 그냥 지면에서 읽었을 때보다 훨씬 잘 기억하게 됨
내게 “스위트 스팟”은 증명의 한 단계를 정당화하는 데 30초에서 5분 정도 걸릴 때임. 그보다 길어지면 좌절하기 쉽고 덜 잘 배우게 됨
실제 논문의 증명을 보기 전까지 기다려보면 됨
좀 더 진지하게 말하면, 물론 잘못 쓰였고 교육적이지 않은 수학책들도 있음. 하지만 평균적인 대학원 수준의 증명은 모든 세부 사항을 다 적을 수 없다고 봄. 그러면 읽기 고되고 극도로 지루해짐
수학자는 머릿속에서 증명의 구멍을 메우는 것이 기대되고, 이 능력은 배워야 함
대다수는 연구 수준 수학을 적어도 읽을 수 있으려고 대학원 수준 수학을 공부하니, 이게 필터로 작동한다면 적어도 강의 지식이 쓰이는 방식의 필터와는 어느 정도 맞물려 있음. 때로는 불행한 일이지만
빈칸 채우기에 관한 개인적인 일화가 몇 개 있음
고등학교 때, 필요한 세부 수준을 두고 논쟁한 뒤 내가 생략을 최소화해 증명을 쓰기로 합의한 적이 있음. 내가 빈칸을 채울 수 있음을 보여주면, 기대보다 더 개요 수준으로 썼던 많은 텍스트도 필요한 이해를 입증하기에 충분한 것으로 인정하기로 했음
적어도 세 겹으로 중첩된 “이건 사실 명시적 증명이 필요 없지만 약속했으니” 괄호를 썼던 기억이 남. 가장 아래쪽 괄호 중 하나에는 “2^n>0임을 귀납법으로 증명하자”가 들어 있었음. 최상위 명제는 아마 극한에 관한 것이었음. 덧붙이면, 가장 아래쪽의 과도한 증명들은 실제로 과도했다는 데 서로 동의함
고등학교와 대학에서 필기할 때, 다음에 당연히 말할 내용의 요지를 미리 적어두고, 그 다음 내용에 더 많은 세부 필기가 필요할 때 시간을 벌곤 했음. 나중에 박사후연구원일 때 동료가 어떤 문제를 설명하는 걸 듣다가 “그 부분은 건너뛰어도 돼, 어떤 보조정리를 말하려는지와 어떻게 증명할지 보인다”고 끊은 적이 있음
알고 보니 틀렸음. 그들은 결과를 주장한 게 아니라 질문하고 있었음. 다만 내가 추측한 개요에서 나온 증명은 결국 논문에 들어가긴 했음
우리처럼 구체적인 수학을 하는 사람들 중에는 Lean, Agda, Coq 같은 증명 보조기로 세부 사항 문제를 고치려는 세계가 따로 있음. 하지만 “일반적인” 수학 교육용으로 증명 보조기를 쓰는 사람은 거의 없을 것 같음. 왜일까?
이산수학에서는 학생들이 컴퓨터과학/이산수학 증명과 더 잘 상호작용하게 하려고 CS 학과에서 그렇게 한다는 경우가 있음
연속수학에서는 표준적인 표현과 고차 논리 증명 보조기 사이에 약간의 표현 불일치가 있음. 1차 집합론 형식화로 충분히 멀리 가려면 필요한 정의들이 있는데, 아직 일관된 모음으로 정리되지는 않은 것 같음
Lobste.rs 의견들
아, 이건 아프다. 개인적인 일화 겸 푸념을 하자면, 내가 수학/컴퓨터과학이 아니라 소프트웨어 엔지니어링을 하게 된 이유 중 하나는 교실에서 구두로 접할 때와 혼자 책으로 볼 때의 수학 이해력 차이가 너무 컸기 때문임
나는 글로 쓰인 정리를 이해하는 데 비정상적으로 많은 시간이 필요하고, 결국 알고 보면 쉬운 내용이 내 취향에는 형편없이 설명되어 있었다는 느낌이라 매우 불만족스러움
다만 내 진단은 조금 다름. 세부 사항이 부족해서가 아니라, 오히려 동기와 개요가 부족한 게 문제라고 봄. 증명은 모두 정확히 거꾸로 쓰인 것처럼 보임. 문제를 오래 고민해 증명을 찾아낸 뒤, 그 사고 과정을 지우고 마지막 단계부터 증명을 쓰기 시작함
예를 들어 증명은 보통 “ɛ = n^2 / 36을 택하자”로 시작해서, 왜 그 엡실론이 기계적으로 필요한지 한 번 읽어야 하고, 그 기술적 장치 뒤의 아이디어를 이해하려고 또 고민해야 하며, 그 아이디어로 머릿속에서 비형식 증명을 해본 다음, 마지막으로 그 아이디어를 염두에 두고 증명이 올바른 형식화인지 다시 읽어야 함. 형식화는 유용하지만, 이해 그 자체는 아님
Reed-Solomon도 예시가 됨. Wiki는 “N차 다항식은 N+1개 점에서 보간 가능하다. K개 점을 중복 전송하면 일부를 잃어도 계수를 복구할 수 있다”고 말할 수 있었는데, 대신 장황한 난해한 설명이 이어짐 (previously)
최근 예로는 Tao의 Analysis 정리 1.5.8, 즉 콤팩트 집합에서는 모든 열린 덮개가 유한 부분덮개를 갖는다는 내용이 있음. 곧바로 “y를 택하고, V_a를 택하고, 공이 있고, 반지름 r이 있고…”로 들어가는데 틀린 말은 아니지만 왜 그렇게 하는지 알기 어려움
형식을 흡수하고 나서야 핵심 아이디어가 보임. 유한 부분덮개가 필요하니 “가장 큰” 집합을 탐욕적으로 고르는 게 자연스럽지만, 가장 크다는 게 무슨 뜻인지 정해야 함. 한 점을 고정하면 그 점에 상대적으로 가장 큰 집합을 고를 수 있고, 공을 키우다 덮개의 원소가 하나만 남게 만들면 됨. 공들이 무한히 작을 수는 없고, 그러면 콤팩트성을 써서 반지름 0인 공을 가진 점을 뽑게 됨. 따라서 공은 최소 ɛ만큼 넓고, 아직 덮이지 않은 점에 대해 가장 큰 집합을 계속 고르면 됨. 유한 단계에서 끝나면 성공이고, 끝나지 않으면 서로 ɛ만큼 떨어진 점들의 수열이 생겨 콤팩트성과 모순됨
핵심 아이디어는 항상 형식화보다 훨씬 단순하고, 일단 그걸 잡으면 부등식을 충분히 다듬으면 어떤 형식화는 당연히 성립할 것처럼 보임. 형식화는 여전히 필요함. 실수로 선택공리 같은 것에 의존했는지 모를 수 있으니까. 하지만 아이디어를 전달하는 수단으로는 형편없음. 마치 퀵 정렬을 어셈블리 코드에서 역추적하는 것 같음
수학을 제시하는 올바른 방식은 정리를 출발점이 아니라 결과로 두고, “어떻게 이걸 발견할 수 있었는가” 모드로 설명하는 것이라고 봄
물론 가끔은 “정말로 이게 증명한다는 걸 납득할 때까지 붙잡고 흔드는” 논증도 있다는 걸 부정하지는 않지만, 내가 접한 비교적 순한 수학 안에서는 그런 경우가 드문 편임
교과서의 정리는 요리책에 실린 완성된 케이크 사진 같고, 증명은 레시피 같음. 케이크를 만들면서 생기는 난장판은 실제로 잘 보이지 않음
빠진 것은 같은 케이크를 구우려면 여전히 제빵에 대한 이해와 기술이 필요하다는 점임. 레시피에는 반죽의 농도나 잘못됐을 때 어떻게 고칠지 같은 내용이 빠질 수 있음. 또한 제빵의 “제1원리”를 안다고 바로 제빵사가 되는 것도 아님. 기본 아이디어는 있어도 그것들을 조합해 케이크를 구워야 함
수학도 다른 현대 학문과 같다고 봄. 진열장에는 케이크가 가득하고, 최고의 제빵사들은 더 많은 케이크를 굽도록 연구비를 받음. 스스로 제빵사가 되려면 빵집에서 견습하며 요령을 배우고, 상사의 레시피만 쓰는 대신 자기 케이크를 굽기 시작해야 함. 여기에는 시간과 노력, 약간의 운이 필요함
https://betterexplained.com/articles/…
DNA 서열은 고양이에 대한 매우 정밀한 설명일 수 있지만, 그것만 보고 그 동물을 머릿속에 그릴 수는 없음
이렇게 포맷하면 검사와 정정이 더 효율적이고, 이를 R-S의 BCH 관점이라고 부름. 다만 BCH는 코드의 한 부류 전체이기도 함
그래도 구현하면서 이 내용을 정말 많이 읽어본 뒤에도 R-S와 BCH에 대한 Wikipedia 문서는 대체로 이해 불가능하다는 데 동의함. 멋진 리터레이트 프로그래밍 방식의 gf256 라이브러리, 특히 gf256::rs가 없었다면 진전이 없었을 것 같음
다만 경험상 어떤 정리는 다른 정리보다 증명하기 쉬움. Algebra I 수업에서는 시험 중 하나가 교수가 즉석에서 고른 임의의 정리를 증명하는 것이었음. 위협적으로 보일 수 있지만, 이미 증명된 것들을 오래 증명하다 보면 패턴이 보이기 시작함. 게다가 다른 증명에 쓰이는 정리도 더 많이 외우게 됨
쉽다는 말은 아니지만, 그 수준에서 수학을 공부하면 머릿속에서 무언가가 열려 가능해지는 느낌이 있음. 형식화가 과해 보일 수는 있어도, 수학자가 다른 사람들이 보지 못하는 결론에 도달할 수 있게 해주는 것이기도 함
물리과학 쪽 개인 경험으로는, 많은 부분이 학술 논문이 쓰이고 출판되고 평가되는 방식에서 온다고 봄
논문 작성과 출판 과정은 실제로 과학을 설명하도록 유도하지 않고, 세부 사항에 시간을 너무 “낭비”하지 않으면서 그럴듯하고 약간 설득력 있어 보이는 말을 하도록 유도함. 증명에서 보이는 이런 편향도 매우 비슷해 보임
출판사를 과학에서 빼야 함
“이걸 어떻게 찾았는가”를 설명하려면 완전히 정당화되지도, 정밀하지도 않은 모호하고 거친 진술을 해야 함. 심사자들은, 그 장소가 자체 출판이지만 색인되는 학회 프로시딩이나 오버레이 저널이어도, 어느 정도 거짓인 문장이 최종 채택본에 남는 것을 꺼림
그래서 첫 제출본에 직관적 설명이 있었더라도 결국 빠지는 일이 생김
더 나쁜 경우도 있음. 서론을 잘 쓰고 논문을 채택되기 좋게 최적화하는 데 능한 내 공저자는, 명제 버전을 고를 때 보통 트레이드오프가 있다고 설명하곤 함. 가장 채택되기 쉬운 버전이 그 논문을 좋아하고 인용할 사람들에게는 최악인 경우가 많음. 모든 버전이 참이고 같은 수준의 증명 품질로 증명될 수 있어도 그렇다
그래서 인센티브가 맞지 않음. 다만 이번에는 출판사 잘못이라기보다, 학자들이 실제로 해야 할 작업이 아니라 출판 지표만으로 보상받는 구조 때문일 수 있음
교과서에 대해서는 글의 주장에 꼭 동의하지 않음. 좋은 생략은 증명을 더 읽기 쉽게 만들고 독자가 생각하도록 유도할 수도 있음. 최악의 경우 다른 교과서나 원전을 보면 됨. 하지만 연구 논문에서 불완전한 증명을 만나면 매우 짜증날 수 있음. 여기서는 누가 정말 전체 증명을 가지고 있는지 의심이 스며들고, 정신 차려보면 일주일/한 달/일 년이 지나 있을 수 있음
수학 대학원생으로서 이 문제에는 양면이 있다고 봄. 때로는 제시된 증명이 꽤 높은 수준이라 특정 단계를 정말 모르겠을 때 짜증나지만, 반대로 빈칸을 채우는 과정이 모든 걸 다 받는 것보다 실력 향상에 더 유용할 때가 있음
증명이 명제 1에서 명제 2로 넘어가는데 바로 이해되지 않으면, 첫째로 저자와 더 나아가 해당 분야의 수학 공동체가 무엇을 자명하다고 여기는지에 대한 직관을 줌. 이는 어떤 결과를 직관적으로 깊이 익혀야 하는지 알려주기 때문에 가치 있음
둘째로 중간 단계를 채워 넣고 논증이 탄탄하다고 스스로 납득하면, 그 중간 단계를 그냥 지면에서 읽었을 때보다 훨씬 잘 기억하게 됨
내게 “스위트 스팟”은 증명의 한 단계를 정당화하는 데 30초에서 5분 정도 걸릴 때임. 그보다 길어지면 좌절하기 쉽고 덜 잘 배우게 됨
실제 논문의 증명을 보기 전까지 기다려보면 됨
좀 더 진지하게 말하면, 물론 잘못 쓰였고 교육적이지 않은 수학책들도 있음. 하지만 평균적인 대학원 수준의 증명은 모든 세부 사항을 다 적을 수 없다고 봄. 그러면 읽기 고되고 극도로 지루해짐
수학자는 머릿속에서 증명의 구멍을 메우는 것이 기대되고, 이 능력은 배워야 함
빈칸 채우기에 관한 개인적인 일화가 몇 개 있음
고등학교 때, 필요한 세부 수준을 두고 논쟁한 뒤 내가 생략을 최소화해 증명을 쓰기로 합의한 적이 있음. 내가 빈칸을 채울 수 있음을 보여주면, 기대보다 더 개요 수준으로 썼던 많은 텍스트도 필요한 이해를 입증하기에 충분한 것으로 인정하기로 했음
적어도 세 겹으로 중첩된 “이건 사실 명시적 증명이 필요 없지만 약속했으니” 괄호를 썼던 기억이 남. 가장 아래쪽 괄호 중 하나에는 “2^n>0임을 귀납법으로 증명하자”가 들어 있었음. 최상위 명제는 아마 극한에 관한 것이었음. 덧붙이면, 가장 아래쪽의 과도한 증명들은 실제로 과도했다는 데 서로 동의함
고등학교와 대학에서 필기할 때, 다음에 당연히 말할 내용의 요지를 미리 적어두고, 그 다음 내용에 더 많은 세부 필기가 필요할 때 시간을 벌곤 했음. 나중에 박사후연구원일 때 동료가 어떤 문제를 설명하는 걸 듣다가 “그 부분은 건너뛰어도 돼, 어떤 보조정리를 말하려는지와 어떻게 증명할지 보인다”고 끊은 적이 있음
알고 보니 틀렸음. 그들은 결과를 주장한 게 아니라 질문하고 있었음. 다만 내가 추측한 개요에서 나온 증명은 결국 논문에 들어가긴 했음
우리처럼 구체적인 수학을 하는 사람들 중에는 Lean, Agda, Coq 같은 증명 보조기로 세부 사항 문제를 고치려는 세계가 따로 있음. 하지만 “일반적인” 수학 교육용으로 증명 보조기를 쓰는 사람은 거의 없을 것 같음. 왜일까?
연속수학에서는 표준적인 표현과 고차 논리 증명 보조기 사이에 약간의 표현 불일치가 있음. 1차 집합론 형식화로 충분히 멀리 가려면 필요한 정의들이 있는데, 아직 일관된 모음으로 정리되지는 않은 것 같음