린

린은 수학 증명을 컴퓨터가 검산할 수 있는 형태로 옮겨 적는 언어예요. 우리가 학교에서 수학 문제를 풀 때 중간 계산 과정을 하나하나 적어야 채점자가 맞았는지 확인할 수 있는 것처럼, 린으로 증명을 쓰면 아주 작은 논리 단계 하나하나까지 빠짐없이 적어야 해요. 그 대신 사람이 눈으로 읽고 실수를 놓칠 위험 없이, 컴퓨터가 기계적으로 한 줄씩 맞는지 틀리는지 확인해줘요.

보통 수학자가 쓰는 증명은 몇 쪽 분량의 글로, 중간중간 '이건 자명하다'거나 '앞서 보인 것과 같은 방식으로'처럼 생략된 부분이 많아요. 사람 독자는 이런 생략을 채워 읽을 수 있지만 컴퓨터는 그럴 수 없어서, 린으로 증명을 옮기려면 생략된 단계까지 전부 펼쳐 써야 해요. 그래서 몇 쪽짜리 증명이 린으로 옮겨지면 수백만 줄짜리 코드가 되기도 해요.

이렇게 빈틈없이 다시 쓰는 작업을 공식화라고 불러요. 사람이 손으로 하면 수년이 걸릴 만큼 지루하고 방대한 일이지만, 한번 린으로 완성되면 그 증명이 정말 맞는지를 두고 더 이상 사람의 판단에 기대지 않아도 돼요.

기사에서는 "클로드가 Lean이라는 증명 언어로 1300만 줄에 이르는 코드를 써냈다"고 나와요. 여기서 린은 앤스로픽이 만든 도구가 아니라, 이미 수학계에서 쓰이던 증명 검증용 언어예요. 클로드는 이 언어의 문법에 맞춰 증명을 써낸 것이지, 린 자체를 새로 만든 게 아니라는 점을 헷갈리지 않아야 해요.