네 가지 정리 증명기 이야기: Isabelle/HOL, Lean, HOL4, Agda에 대한 (적당히) 주관적인 비교

요약

AI가 인간의 지적 활동과 공동체를 해체하며 개인의 기여와 인정이라는 동기를 약화시킬 수 있음을 경고합니다.
지적 활동은 공유된 지식과 타인에게 기여하는 보람이라는 공동체적 자원에 의존하므로, AI가 이를 대체하면 지속 가능한 지적 문화가 사라질 위험이 있습니다.

개인의 지적 활동을 오래 지속하려면 인간 공동체가 필요하며, AI가 공동체를 해체하면 혼자 배우고 만드는 활동도 줄어듦
AI 에이전트에 업무를 맡기고 취미로 프로그래밍을 계속하리라는 기대와 달리, 함께 읽고 배우고 만들어갈 공동체가 약해지면 개인의 즐거움만으로 활동을 이어가기 어려움
블로그, 라이브러리, 새 언어를 AI가 흡수하거나 대신 사용하고 기여자를 드러내지 않는다면, 공동의 인간적 작업에 참여한다는 감각도 사라짐
지적 활동에는 타인이 쌓은 지식뿐 아니라 자신의 작업이 누군가에게 도움이 된다는 보람과 인정이 필요하며, 이 관계가 개인과 공동체를 함께 유지함
공동체가 무너져도 순수한 내적 동기를 가진 사람만 남으리라는 낙관론은, 인간이 타인과의 관계 속에서 동기를 얻는 사회적 존재라는 점을 놓침

처음에는 AI가 소프트웨어 엔지니어링을 해결하더라도 직업과 개인 활동을 나눌 수 있으리라 기대했음
- 직업에서는 원하는 것을 기술하고 AI 에이전트가 코드를 작성하도록 관리
- 개인 시간에는 기술 블로그와 논문 읽기, 프로그래밍 언어 학습과 설계, 에세이 작성, 작은 오픈소스 프로젝트를 즐거움으로 계속함
그러나 개인 활동에 대한 기대는 충분히 실현되지 않았음
앞선 글에서 다룬 변화에는 생산성 향상과 사회적 손실이 공존
- 더 어수선한 코드베이스라는 대가가 있어도 단위 노력당 산출물은 늘어남
- 컴파일러, 타입 시스템, 논리 대신 프롬프트와 에이전트 실행 환경, 반복 루프가 논의의 중심이 되면서 내용은 더 좁고 얕고 반복적으로 변함
코드를 작성하며 실력과 사고력을 쌓던 과정도 약해짐
- 컴퓨터가 코드를 대신 작성하면 코딩을 배울 유인이 줄어듦
- 좋은 프로그래머가 되기 위해 연습하던 엄밀하고 체계적인 사고까지 기계에 맡기고, 사람은 감에 의존하게 됨

AI 이전에는 오픈소스 코드, 블로그, 튜토리얼, 포럼 글과 교과서로 다른 사람에게 기여할 수 있었음
AI가 생산과 지식 전달을 대신할수록 그 기여의 의미가 약해짐
- 블로그: 기술적 해결책이 학습 데이터에 흡수되고, 다음 사람은 Claude에게 답을 얻지만 기여자는 드러나지 않음
- 새 프로그래밍 언어: 사람이 코드를 쓰거나 읽지 않으면 언어는 인간이 신경 쓸 필요 없는 구현 세부사항이 됨
- 라이브러리: AI가 찾아 사용해도 운영자는 누가 만들었는지 모를 수 있음
문제는 GitHub 스타나 블로그 방문자 수만이 아니라, 공동의 인간적 작업에 참여한다는 감각의 상실
AI와 함께 개인의 코드 정원을 끝없이 키울 수 있지만, 정원을 나와 다른 사람과 교류하고 교환하는 장터에 갈 필요가 없어짐
이런 조건에서는 무언가에 관심을 갖고 행동하기 어려워짐
코딩이 고역이었다면 수학 같은 더 높은 활동으로 옮겨가면 된다는 반론도 있지만, 수학에서도 비슷한 변화가 진행 중

지적 활동은 혼자 앉아 세계를 처음부터 생각해 내는 일처럼 보이지만, 고립된 상태에서는 얻을 수 없는 두 가지 자원에 의존함
- 공유된 지식과 성과: 모든 지식의 발전 과정을 혼자 다시 밟지 않고, 다른 사람의 작업 위에 쌓을 수 있는 기반
- 동기: 배우고 만드는 즐거움과, 다른 사람에게 기여하려는 마음
내적 동기는 배움 자체의 즐거움이나 창작 충동처럼 활동 안에서 생김
외적 동기는 돈과 명성만을 뜻하지 않음
- 자신의 능력으로 타인을 돕고, 다른 사람이 작업의 혜택을 받으며, 공동의 프로젝트에 기여하려는 마음도 포함
- David Chapman의 ‘고귀함, nobility’도 자신의 능력을 타인을 위해 사용하는 것과 연결됨
- 명성과 동료의 존중, 호의는 자신의 기여가 유용했는지 가늠하는 지표가 됨
내적 동기도 감정이므로 일시적이며, 영감이 영원히 이어지는 것은 아님
외적 동기가 영감과 영감 사이의 공백을 메우고 활동을 지속시킴

지속적이고 복잡한 지적 활동에는 연료와 산화제처럼 재료와 동기를 공급하는 공동체가 필요함
개인의 활동도 다시 공동체를 유지
- 논문, 교과서, 코드를 공개하면 다른 사람이 쌓아갈 공유 자산이 늘어남
- 논문을 인용하거나 저장소에 기여하면 상대에게 유용한 일을 했다는 인정과 계속할 동기를 줌
공동체가 사라진다고 각자가 고립된 채 자기 일을 계속하는 것은 아님
공유 자산을 보태는 사람과 자신의 작업에서 혜택을 받을 동료가 사라지면, 지적 활동을 지속할 자원도 고갈됨
내적 동기만으로 오래 버티기 어려우므로, 외적 동기의 상실은 개인의 지적 활동 감소로 이어짐

AI가 지적 작업을 대신하는 미래에는 인간의 기여가 불필요하거나 중복된 것으로 밀려남
소프트웨어에서는 AI가 코드를 쓰고 사람이 작성하지 않는다면, 코딩 블로그와 튜토리얼을 읽거나 새 라이브러리와 언어를 사용할 인간 독자층도 줄어듦
수학에서도 AI가 정리를 증명하고 논문을 쓰고 해설하며 학생을 가르칠 수 있고, 가까운 미래에는 인간보다 나은 교과서를 쓸 수도 있음
새 언어나 논문을 만들어도 달라지는 것이 없고 기여할 공동체도 없다면, 활동을 이어갈 이유가 사라짐
다른 지적 영역에서도 같은 변화가 이어진다면, 개별 활동은 남아도 살아 있는 공동 문화는 사라질 수 있음
- 라이브러리와 프로그래밍 언어를 만드는 개인은 있어도 공유된 소프트웨어 엔지니어링 문화는 없음
- 수학을 공부하고 실천하는 개인은 있어도 살아 있는 수학자 공동체는 없음