이 글의 영문 버전을 린 커뮤니티에 올렸었는데, 커뮤니티 관리자가 그 글을 삭제했습니다. 그 뒤에 어느 한 관리자가 제게 개인 메시지를 보내 제가 이와 비슷한 글을 또 올리면 계정을 정지하겠다고 경고했습니다.
제재 사유는 제가 아동 성 학대라는 중범죄를 너무 가벼이 다뤘기 때문이라고 하네요. 저는 법 개정안과 현행법을 비교하는 데 증명 보조기를 활용하는 일이 아동 성 학대를 가벼이 다룬다고 생각하지 않습니다.
증명 보조기[proof assistant]라는 컴퓨터 프로그램은 보통 소프트웨어 검증이나 수학 증명의 재서술(형식화)에 쓰이는데, 아마 린(Lean) 증명 보조기를 아청법 개정안을 구상하는 데 활용한 사람은 제가 최초일 것입니다.
그러다 보니, 법률가는 린 코드를 읽을 줄 모르고, 린을 다룰 줄 아는 수학자·컴퓨터 과학자·논리학자는 당연히 아청법의 일부 조항을 형식화한 린 코드를 검토할 의향이 전혀 없습니다.
저는 증명 보조기가 더 많은 사람이 이용하기 편리해진다면, 그것이 이공계 밖의 분야, 특히 철학이나 법학에서도 활발히 쓰이는 날이 올 것으로 전망합니다. 제가 작성한 린 코드가 증명 보조기의 잠재성을 보여 준다고 저는 생각해요.
저는 고졸자이고 학계 밖에 있지만, 앞으로 증명 보조기의 활용 방안을 다양한 분야의 종사자에게 소개하는 데 힘쓰겠습니다.
- 깃 저장소: https://git.sr.ht/~chabulhwi/lean-notes
- 영어 문서: https://git.sr.ht/~chabulhwi/lean-notes/tree/master/item/docs/en/CYSEM.md
- 한국어 문서: https://git.sr.ht/~chabulhwi/lean-notes/tree/master/item/docs/ko/CYSEM.md
- 린(Lean) 언어로 작성한 코드: https://git.sr.ht/~chabulhwi/lean-notes/tree/master/item/Notes/CYSEM.lean
- 린 4 웹 편집기서 린 코드 살펴보기: Lean 4 Web
아동·청소년 성 착취물 재정의하기
아동·청소년의 성보호에 관한 법률
'아동·청소년의 성보호에 관한 법률'(법률 제20462호, 2025년 4월 17일 시행)에서, '아동·청소년 성 착취물'은 다음과 같이 정의됩니다.
제2조(정의) 이 법에서 사용하는 용어의 뜻은 다음과 같다. <개정 2012. 12. 18., 2014. 1. 28., 2018. 1. 16., 2020. 5. 19., 2020. 6. 2., 2021. 3. 23., 2024. 3. 26., 2024. 10. 16.>
- “아동·청소년”이란 19세 미만의 사람을 말한다.
[중략]- “아동·청소년성착취물”이란 아동·청소년 또는 아동·청소년으로 명백하게 인식될 수 있는 사람이나 표현물이 등장하여 제4호 각 목의 어느 하나에 해당하는 행위를 하거나 그 밖의 성적 행위를 하는 내용을 표현하는 것으로서 필름·비디오물·게임물 또는 컴퓨터나 그 밖의 통신매체를 통한 화상·영상 등의 형태로 된 것을 말한다.
제4호의 각 목은 다음과 같습니다.
가. 성교 행위
나. 구강·항문 등 신체의 일부나 도구를 이용한 유사 성교 행위
다. 신체의 전부 또는 일부를 접촉·노출하는 행위로서 일반인의 성적 수치심이나 혐오감을 일으키는 행위
라. 자위 행위
아동·청소년 성 착취물 재정의하기
아동·청소년 성 착취물의 정의를 어떻게 고칠지에 관한 문서를 제가 작성했습니다.
그 글에서, 저는 제2조 제5호를 다음과 같이 개정할 것을 제안했습니다.
- 텍스트는 아동·청소년 성 착취물의 범주에 들어가지 않음을 명시함.
- 실제 아동·청소년 성 착취물의 범주에만 인쇄물을 넣음. 그러나 만화 캐릭터만 이용해 만든 아동·청소년 성 착취물의 범주에는 여전히 인쇄물이 안 들어감.
- 가상의 캐릭터만 이용해 만든 아동·청소년 성 착취물은 하등의 문학적·예술적·사상적·과학적·의학적·교육적 가치를 지니지 않음을 명시적으로 서술함.
CYSEM 파일에서, 저는 린 정리 증명기를 이용해 다음 주장을 형식화했습니다.
- 성인이나 가상의 캐릭터만 이용해 만든 가상 아동·청소년 성 착취물은 정의상(定義上) 음란하다. (
Depiction.isObscene_of_isVirtualCYSEM) - 가상 아동·청소년 성 착취물은 하등의 가치를 지니지 않는다. (
Depiction.lacksValue_of_isVirtualCYSEM) - 제2조 제4호의 변경 사항을 제외하면, 현행 아청법에 따른 아동·청소년 성 착취물의 정의는 차불휘가 제안한 정의와 논리적으로 동등하다. 그 정의에 따르면, 아동·청소년 성 착취물은 (1) 실제 아동·청소년 성 착취물 또는 (2) 하등의 가치를 지니지 않는 가상 아동·청소년 성 착취물을 일컫는다. (
Depiction.isCYSEM_iff_isRealCYSEM_or_isVirtualCYSEM_and_lacksValue)
실제 아동·청소년의 성적 행위를 시각적으로 묘사한 표현물에 관한 제 추측도 형식화했습니다. 그 추측의 내용은 다음과 같습니다. "그런 표현물은 모두 음란하다." (ObsceneVisualDepiction.real_childOrYouth_conjecture)
중요한 전제와 보조 정리
몇 가지 중요한 전제와 보조 정리를 아래에 나열했습니다.
중요한 전제
- 모든 음란물은 하등의 가치를 지니지 않는다. (
Depiction.lacksValue_of_isObscene) - 포르노그래피는 음란하다. [
Depiction.isObscene_of_isPorn, 이 전제는 영문으로 번역된 아청법 조항을 분석하는 데 필요함] - 아동·청소년 성 착취물은 아동·청소년 이용 음란물과 동등하다. (
Depiction.isCYSEM_iff_isCYP)
중요한 보조 정리
- 아동·청소년 이용 음란물은 음란하다. (
Depiction.isObscene_of_isCYP) - 가상 아동·청소년 성 착취물은 아동·청소년 성 착취물이다. (
Depiction.isCYSEM_of_isVirtualCYSEM)
참고 문헌
- 아동·청소년의 성보호에 관한 법률. 2025. 4. 17. 시행. 법률 제20462호, 2024. 10. 16., 일부개정.
https://elaw.klri.re.kr/kor_service/lawView.do?hseq=68811&lang=KOR.