보조정리 (Lemma)

보조정리(lemma, 음차 '렘마')는 주된 정리를 증명하는 과정에서 디딤돌로 쓰기 위해 따로 떼어 먼저 증명하는 명제입니다. 수학적으로는 정리와 똑같이 증명된 참인 명제이며, '정리(theorem)', '따름정리(corollary)', '명제(proposition)'와의 차이는 논리적 지위가 아니라 문서 안에서의 역할과 중요도입니다.

자세히 알아보기

긴 증명을 하나의 덩어리로 쓰면 검증하기 어렵습니다. 그래서 수학자들은 증명을 작은 단계로 나누고, 반복해서 쓰이거나 독립적으로 의미 있는 단계를 보조정리로 분리합니다. 이렇게 하면 각 단계를 따로 확인할 수 있고, 다른 증명에서도 재사용할 수 있습니다. 컴퓨터로 증명을 검증하는 형식 증명(Lean, Coq 등)에서도 큰 정리를 수많은 보조정리로 쪼개 쌓아 올립니다.

일부 보조정리는 원래 목적보다 더 유명해졌습니다. 조른의 보조정리, 유클리드의 보조정리(소수 p가 ab를 나누면 a나 b를 나눈다), 슈바르츠-지펠 보조정리 등이 그 예입니다.

블록체인·암호화폐에서는

현대 암호의 '증명 가능한 안전성'은 보조정리들의 사슬로 이루어집니다.

• 포킹 보조정리(forking lemma): 포인슈발과 스턴이 제시한 이 보조정리는 '서명을 위조할 수 있는 공격자를 같은 무작위성으로 두 번 실행하되 랜덤 오라클(해시)의 응답만 바꾸면, 얻은 두 위조 서명으로 이산 로그를 풀 수 있다'는 논증을 정식화합니다. 비트코인 탭루트가 채택한 슈노어 서명(BIP-340)의 안전성 논증이 이 보조정리에 기대고 있습니다.
• 슈바르츠-지펠 보조정리: 0이 아닌 d차 다항식이 무작위 점에서 0이 될 확률은 d/|F| 이하라는 결과입니다. zk-SNARK·STARK와 KZG 다항식 약정은 '무작위 점 하나에서 같으면 두 다항식은 거의 확실히 같다'는 이 보조정리로 거대한 계산을 짧게 검증합니다.
• 잔여 해시 보조정리(leftover hash lemma): 엔트로피가 충분한 입력을 범용 해시로 압축하면 거의 균일한 비트를 얻는다는 결과로, 난수 추출기 설계의 근거입니다.

쉽게 말하면

보조정리는 큰 다리를 놓기 전에 먼저 세우는 교각입니다. 교각 하나하나가 튼튼해야 다리 전체가 섭니다.

예시

'√2는 무리수다'를 증명할 때 먼저 '정수 n²이 짝수이면 n도 짝수다'를 보조정리로 증명해 두고, 본 증명에서 두 번 사용합니다.

또 다른 예로, 슈바르츠-지펠 보조정리는 체의 크기가 약 2²⁵⁵일 때 차수가 100만(약 2²⁰)인 다항식이 무작위 점에서 우연히 0이 될 확률이 2⁻²³⁵ 이하임을 보장합니다. 영지식 증명의 건전성 계산이 이런 식으로 이뤄집니다.