💻 computer science

A Formalization of the Laplace Transform and Its Inversion in Lean 4

이 논문은 라플라스 변환과 브롬위치 유형의 정리를 통한 그 역변환에 대한 Lean 4 정식화를 제시하며, 주요한 해석적 및 정식화 측면의 과제들을 다루면서 조화 진동자에 대한 적용을 입증한다.

원저자: Daniel Goldberg, Antoine Vinciguerra

게시일 2026-08-10

📖 5 분 읽기🧠 심층 분석

원저자: Daniel Goldberg, Antoine Vinciguerra

원본 논문은 CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/) 라이선스로 제공됩니다. ✨ 이것은 아래 논문에 대한 AI 생성 설명입니다. 저자가 작성하거나 승인한 것이 아닙니다. 기술적 정확성을 위해서는 원본 논문을 참조하세요. 전체 면책 조항 읽기

진동하는 진자, 기타 줄의 떨림, 혹은 전선을 타고 흐르는 신호처럼 시간이 지남에 따라 변화하는 사물들의 무질서하고 혼란스러운 움직임을 즉각적으로 깔끔하고 정적인 대수 문제로 변환할 수 있는 세상을 상상해 보십시오. 이것이 바로 공학자와 과학자들이 한 세기 넘게 사용해 온 수학적 도구인 **라플라스 변환(Laplace transform)**의 마법입니다. 이것을 '시간'의 언어(사물이 움직이고, 속도가 빨라지거나 느려지는 곳)로 쓰인 이야기를 '복소수'의 언어(그러한 움직임이 단순한 곱셈과 나눗셈이 되는 곳)로 된 이야기로 번역하는 보편적인 번역기라고 생각하십시오.

이것이 왜 중요할까요? 왜냐하면 사물이 어떻게 변하는지에 대한 방정식을 푸는 것은 엉킨 매듭을 잡아당기며 푸는 것만큼이나 매우 어렵기 때문입니다. 하지만 그 매듭을 단순한 직선처럼 보이는 다른 언어로 번역할 수 있다면, 문제를 쉽게 풀고 나서 그 답을 다시 번역할 수 있습니다. 이 논문은 이 번역기에 대한 '증명 검사기(proof-checker)'를 구축하는 것에 관한 것입니다. 저자들은 단순히 규칙을 적어 내려간 것이 아니라, Lean 4라는 컴퓨터 프로그램을 사용하여 이 번역기가 약속된 대로 정확하게 작동한다는 것을 단계별로 수학적으로 증명했습니다. 그들은 우리가 다리, 회로 또는 제어 시스템을 설계할 때 사용하는 이 강력한 도구들을 사용할 때, 그 기저에 깔린 수학이 견고하며 숨겨진 오류가 없음을 확인하고자 했습니다.

디지털 증명 검사기

매우 엄격하고 매우 문자 그대로의 성격을 가진, 수학을 좋아하지만 추측하는 것은 싫어하는 로봇 친구가 있다고 상상해 보십시오. 당신이 그에게 "여기에 꼬불꼬불한 선을 매끄러운 곡선으로 바꾸는 공식이 있어"라고 말하면, 로봇은 "확실합니까? 만약 선이 너무 많이 꼬불거린다면 어떡하죠? 만약 선이 영원히 계속된다면요?"라고 되묻습니다. 이 논문은 두 명의 연구자, 다니엘(Daniel)과 앙투안(Antoine)이 이 로봇 친구에게 라플라스 변환에 필요한 모든 것을 가르친 결과물입니다.

그들은 단순히 교과서를 쓴 것이 아니라, Lean 4로 구성된 완전한 컴퓨터 검증 라이브러리를 구축했습니다. Lean 4는 컴퓨터가 오류를 확인할 수 있는 수학적 증명을 작성하기 위해 특별히 설계된 프로그래밍 언어입니다. 그들의 목표는 함수를 복소수의 함수로 바꾸는 방법인 라플라스 변환을 가져와서, 기본적인 정의부터 답을 다시 시간으로 돌려놓는 복잡한 '역변환(inversion)' 과정에 이르기까지 모든 규칙이 제대로 작동함을 증명하는 것이었습니다.

번역기와 마법 거울

라플라스 변환은 마법 거울과 같습니다. 함수 $f(t)$ (시간에 따라 일어나는 일을 설명하는 것)를 거울에 넣으면, 거울은 새로운 함수 $(Lf)(s)$(동일한 현상을 '주파수' 세계에서 설명하는 것)를 반사해 냅니다.

순방향 여정: 이 논문은 어떤 함수가 착하게 행동한다면(즉, 너무 빨리 무한대로 폭발하지 않는다면) 거울이 작동한다는 것을 증명합니다. 그들은 상수, 시간의 거듭제곱, 심지어 사인파와 같은 단순한 것들을 어떻게 번역하는지에 대한 규칙을 증명했습니다. 예를 들어, 그들은 미분(변화율)이 숫자 $s$ 를 곱하는 단순한 연산과 시작값을 빼는 것으로 변환됨을 보여주었습니다. 이것이 미분 방정식을 푸는 것을 매우 쉽게 만드는 '비법 소스'입니다.
역방향 여정 (역변환): 진짜 도전은 답을 다시 가져오는 것입니다. 거울에 비친 모습을 보고 원래의 물체가 무엇이었는지 어떻게 알 수 있을까요? 이것을 **역 라플라스 변환(inverse Laplace transform)**이라고 합니다. 이 논문은 **브롬위치 공식(Bromwich formula)**이라 알려진 특정 방법을 증명합니다.

왜 '쉬운' 길을 택하지 않았는가

보통 수학자들은 **복소 경로 적분(complex contour integration)**이라는 기술을 사용하여 역변환 공식을 증명합니다. 지도의 어떤 모양 주위에 루프를 그리고 특수한 정리인 유수 정리(Residue Theorem)를 사용하여 그 안의 '보물'을 세는 것을 상상해 보십시오. 이는 강력한 도구이지만, 저자들은 컴퓨터 라이브러리에 아직 이러한 '지도 그리기' 도구들이 충분히 구축되어 있지 않다는 것을 발견했습니다.

그래서 그들은 더 지면과 가까운, 다른 경로를 택했습니다. 복소 평면에 루프를 그리는 대신, 그들은 이 문제를 실수 범위에서의 적분 문제로 다루었습니다. 그들은 문제를 관리 가능한 작은 조각들로 나누었습니다:

절단(Truncation): 그들은 무한한 선이 마치 $-T$ 에서 $T$ 까지의 짧고 유한한 구간인 것처럼 가정했습니다.
Sinc 함수: 이 구간을 점점 더 길게 만들면서, sinc 함수(점점 작아지는 파동처럼 보이는 함수)와 관련된 특정 패턴이 나타났습니다.
디리클레 적분(Dirichlet Integral): 그들은 이 sinc 파동 아래의 면적에 관한 유명하고 이미 증명된 사실인 디리클레 적분에 의존하여, 구간이 무한히 길어짐에 따라 결과가 원래의 함수를 완벽하게 재구성함을 보여주었습니다.

이 접근 방식은 설정하기는 더 어려웠지만, 컴퓨터가 이미 잘 수행하고 있는 실수 미적분에 의존했기 때문에 컴퓨터가 검증하기에는 더 안전했습니다.

흔들리는 진자 테스트

그들의 시스템이 실제로 작동하는지 증명하기 위해, 그들은 단순히 추상적인 수학을 체크한 것이 아니라 고전적인 물리 문제인 **조화 진동자(harmonic oscillator)**를 풀었습니다.

설정: 그들은 정지 상태에서 시작하지만 빠른 충격을 받는 스프링을 정의했으며, 이는 방정식 $y''(t) + \omega^2 y(t) = 0$ 으로 설명됩니다.
번역: 그들은 이 방정식을 컴퓨터로 검증된 라플라스 번역기에 입력했습니다.
결과: 컴퓨터는 이 복잡한 미분 방정식을 단순한 대수 방정식인 $(s^2 + \omega^2)Y(s) = \omega$ 로 성공적으로 변환했습니다.
해법: $Y(s)$ 에 대해 풀면 $\frac{\omega}{s^2 + \omega^2}$ 를 얻었습니다.
검증: 컴퓨터는 그다음 자신의 라이브러리를 확인하여, 이 특정 결과가 정확히 $\sin(\omega t)$ 의 라플라스 변환임을 확인했습니다.

이것은 큰 성공이었습니다. 이는 컴퓨터가 단순히 답을 계산한 것이 아니라, 그 답이 실제로 사인파라는 것을 증명했다는 것을 의미합니다. 이는 인간 물리학자들이 수 세기 동안 알고 있었던 사실과 일치하면서도, 인간의 실수가 끼어들 틈이 없는 수준의 확실성을 보여준 것입니다.

게임의 엄격한 규칙

이 논문은 당신이 추측을 멈추고 증명을 시작할 때 얼마나 주의를 기울여야 하는지에 대한 교훈이기도 합니다. 저자들은 교과서에서는 흔히 간과되는 몇 가지 '함정'들을 강조합니다:

무한대는 까다롭다: 적분이 무한대로 간다고 그냥 가정해서는 안 됩니다. 증명은 함수가 충분히 빠르게 감소하여 적분의 '꼬리' 부분이 사라져야 한다는 것을 명시적으로 밝혀야 했습니다.
경계 사례: 수학을 수행할 때, 규칙이 변하는 특정 지점(예: $t=0$ )이 있습니다. 컴퓨터는 함수가 정확히 어디에서 정의되고 연속적인지에 대해 엄밀해지도록 강제했습니다.
순서 바꾸기: 역변환 증명에서, 그들은 두 적분의 순서를 바꿔야 했습니다. 일반적인 수학에서는 그냥 이렇게 할 수도 있습니다. 하지만 그들의 형식적 증명에서는, 결합된 곡면 아래의 '면적'이 유한하다는 것을 엄격하게 증명하기 전까지는 순서를 바꿀 수 없었습니다.

결론

이 논문은 **형식 검증(formal verification)**의 이정표입니다. 이 논문은 새로운 물리 법칙을 발견하거나 새로운 유형의 파동을 발명하는 것이 아닙니다. 대신, 이미 널리 사용되고 있는 도구 주변에 확실성의 요새를 구축하는 것입니다. 라플라스 변환과 그 역변환을 컴퓨터가 확인할 수 있는 언어로 번역함으로써, 저자들은 참조 표준을 만들었습니다.

그들은 함수가 무한대에서 어떻게 행동하는지, 그리고 시작점에서 어떻게 행동하는지에 대한 엄격한 규칙을 따른다면 이 '마법 거울'이 작동한다는 것을 증명했습니다. 그들은 답으로 가는 경로가 지름길보다는 신중하고 단계적인 논리를 포함한다는 것을 보여주었습니다. 이러한 수학적 도구에 의존하는 차세대 소프트웨어를 구축하는 모든 이들에게, 이 연구는 그 토대가 단순히 강할 뿐만 아니라 깨지지 않는다는 것을 보장합니다. 조화 진동자 예시는 최종 승인 역할을 합니다: 컴퓨터는 인간과 의견이 일치하며, 처음으로 컴퓨터가 그 증명에 서명했습니다.

기술 요약: Lean 4에서의 라플라스 변환 및 그 역변환의 형식화

문제 정의
본 논문은 mathlib 라이브러리를 활용하여 Lean 4 정리 증명기 내에서 라플라스 변환과 그 역변환을 형식화하는 문제를 다룬다. 라플라스 변환은 선형 미분 방정식을 대수 방정식으로 변환하는 표준적인 도구이지만, 이를 엄밀하게 형식화하는 것은 상당한 어려움을 수반한다. 이러한 어려움에는 복소수 값 함수 처리, 부적절 적분(truncated integral의 극한과 르베그 적분 간의 관리), 그리고 현재 Lean 4 라이브러리에서 충분히 발달하지 않은 복소 경로 적분 및 유수 정리(residue theorems)에 의존하지 않고 역변환 정리를 증명하는 문제가 포함된다.

방법론
저자들은 mathlib에서 사용 가능한 보크너 적분(Bochner integral) 프레임워크에 기반한 측도론적 접근 방식을 채택한다. 개발 과정은 다음과 같은 몇 가지 핵심적인 방법론적 선택을 통해 진행된다:

추상 커널 구축: 변환은 먼저 커널 $e^{-L(e,p)}$ 를 사용하여 완전 노름 대수(complete normed algebra) $E$ 상의 일반적인 환경에서 정의된다. 이 추상 계층은 지수 커널의 대수적 성질을 특정 측도론적 선택으로부터 분리한다.
실수 값 함수로의 특수화: 구성은 실수 직선 상의 복소수 값 함수로 특수화된다. 저자들은 두 가지 표현을 활용한다:
- 사상된 측도(mapped-measure) 접근법: 역변환 정리를 위해 주로 사용되며, $[0, \infty)$ 상의 르베그 측도를 $\mathbb{C}$ 내의 실수축으로 밀어낸(push forward) 방식이다.
- 직접 집합 적분(direct set-integral) 접근법: 연산 규칙과 조화 진동자 예제에 사용되는 $(0, \infty)$ 상의 적분 방식이다.
부적절 적분 처리: 형식화는 라플라스 변환을 직접적인 부적절 적분 표기법이 아닌, 절단된 적분(truncated integrals, $(0, T]$ 상의 적분)의 극한으로 명시적으로 취급한다. 이 구분은 Lean 프레임워크 내에서 지배 수렴 정리(Dominated Convergence Theorem)를 정확하게 적용하는 데 매우 중요하다.
실수 변수 역변환: 저자들은 복소 해석적 경로 변형과 유수 정리를 사용하는 표준적인 증명 대신, 실수 변수 적분을 사용하여 역변환 정리를 증명한다. 브로미치 경로(Bromwich contour)를 $s = \gamma + ir$ $s = γ + i r$ 로 매개변수화함으로써, 수직선 적분을 $r \in \mathbb{R}$ $r \in R$ 에 대한 적분으로 변환한다. 증명은 다음을 기반으로 한다:
- 적분 순서를 교체하기 위한 푸비니 정리(Fubini's Theorem).
- 진동하는 커널 $\frac{\sin(T(t-a))}{t-a}$ 를 처리하기 위한 디리클레 적분(Dirichlet integral, 별도의 모듈 [9]에서 형식화됨).
- 원래 함수로의 점별 수렴을 보이기 위한 부분 적분 및 디리클레 적분 원시 함수의 성질.

주요 기여
본 논문은 수학 공동체에 네 가지 주요 기여를 제시한다:

일반화된 변환 형식화: 스칼라 및 가법 법칙의 증명을 포함하여, 완전 노룸 대수 상의 라플라스 커널 및 변환에 대한 정의를 제공한다.
연산 규칙 및 수렴: 보크너 적분을 통한 양의 반직선 상의 변환 형식화이다. 저자들은 절단된 변환의 수렴을 증명하고 상수, 거듭제곱, 지수, 미분(반복 미분 포함), 삼각함수(사인 및 코사인), 그리고 스케일링에 대한 폐쇄형 공식을 확립한다. 이러한 증명은 명시적인 적분 가능성 및 붕괴(decay) 가정 하에 수행된다.
브로미치 유형 역변환 정리: 주어진 집합 $S \subset (0, \infty)$ 의 모든 점에서 미분 가능한 함수 $f(t)$ 를 회복하는 역 라플라스 변환의 형식적 증명을 제공한다. 이 증명은 형식화된 디리클레 적분을 활용하며, 복소 경로 적분을 피하고 대신 실수 매개 적분과 지배 수렴 정리에 의존한다.
조화 진동자 응용: 초기 조건 $y(0)=0, y'(0)=\omega$ 를 갖는 조화 진동자 방정식 $y''(t) + \omega^2 y(t) = 0$ 의 라플라스 도메인 해를 구하는 완전한 형식적 유도를 제시한다. 이 정리는 교과서적 유도에서 흔히 생략되는 모든 해석적 가설(정칙성, 적분 가능성, 붕괴)을 명시적으로 검증한다.

결과
형식적 개발은 네 개의 소스 파일에 걸쳐 약 2,900줄의 Lean 코드로 구성된다. 주요 결과는 다음과 같다:

정리 RealLaplaceTransformIs: 추상적 구성을 익숙한 적분 형태로 전개한다.
정리 IsInverseLaplace: $f(t)$ 와 그 도함수의 연속성, 미분 가능성 및 $f(t)e^{-\gamma t}$ 의 적분 가능성 조건 하에서 역 변환의 점별 수렴을 확립한다.
정리 harmonic_oscillator_laplace_eq: 조화 진동자 방정식을 만족하는 함수의 라플라스 변환이 $\sin(\omega t)$ 의 변환과 같음을 증명한다.

의의 및 범위
저자들은 이 연구를 응용 해석의 형식화를 위한 기초적인 단계로 규정한다. 그 의의는 다음과 같다:

간극 메우기: 완전한 복소 유수 이론의 발전을 기다리지 않고도 Lean 4에서 작동하는 역변환 정리를 제공한다.
명시적 가설: 고전적인 처리 방식에서는 암묵적인 해석적 조건들(경계 붕괴 및 가중 도함수의 적분 가능성 등)을 드러냄으로써 엄밀한 정확성을 보장한다.
모듈형 구조: 추상 커널, 실수축 특수화, 응용 예제의 분리는 향후 발전을 위한 재사용 가능한 구조를 생성한다.

논문은 결론에서 합성곱(convolution) 및 기타 연산 규칙이 자연스러운 다음 단계이지만, 세심한 처리가 필요하여 본 원고에서는 다루지 않았음을 밝힌다. 본 작업은 모든 라플라스 변환의 속성을 담은 포괄적인 라이브러리라기보다, 순방향 변환, 역변환 정리, 그리고 전형적인 응용 사례에 대한 구체적인 형식화로 제시된다.