수학 증명보조기 LEAN

며칠 전에 Quanta magazine 팟캐스트https://www.quantamagazine.org/can-computers-be-mathematicians-20220629/를 듣다가 LEAN이라는 것의 존재성을 알게 됐다.

사실 듣다가 졸아서 정확히 무슨 얘기인지 파악은 못했지만, 궁금해져서 찾아봤다.

우선 LEAN 홈페이지는 https://leanprover.github.io/이다.

근데 처음 검색했을 때 저 페이지 말고 https://leanprover-community.github.io/index.html가 먼저 떴는데, 시작하기에는 여기가 더 좋은 것 같다.

수많은 영어를 헤치고... 시작하기에 제일 좋은 방법이 The Natural Number Game이라는 튜토리얼 비슷무리한 것을 진행하는 것임을 깨달았다. (그리고 여기까지밖에 안 했다.)

https://www.ma.imperial.ac.uk/~buzzard/xena/natural_number_game/

The Natural Number Game

튜토리얼 월드에서 시작해서 덧셈, 곱셈, 함수... 이런 것들을 다룬다. 다 깨는데 한 5시간 걸린 것 같다. 설명이 굉장히 자세하기 때문에 하라는 대로 열심히 따라가면 된다.

어떤 느낌인지만 살펴보자.

가장 간단하게, 목표는 x*y+z=x*y+z임을 보이는 것이다.

LEAN에는 'tactic'이라는 것이 있다. 말 그대로 기술이다. X=X임을 보이는 tactic은 'refl'이다. reflection에서 따온 말이다. 위의 목표를 달성하기 위해서는 코드 창에 refl, 만 입력하면 된다. (C나 JAVA에서 세미콜론을 사용하는 것처럼, LEAN에서는 쉼표를 사용한다.)

또 다른 tactic으로는 rewrite인 'rw'가 있다. 이는 h : A=B라는 명제 혹은 증명이 있을 때, rw h,를 입력하면 식의 A를 B로 바꿔준다. 

그리고 theorem들을 불러와서 사용할 수 있다. 예를 들어 add_zero는 자연수(mynat) a에 대해, a+0=a라는 정리 혹은 증명이다.

• add_zero (a : mynat) : a + 0 = a

a+(b+0)=a+b 임을 보여야 한다고 가정하자.

rw add_zero,를 입력하면 _+0 꼴의 식을 rewrite해줘서 위의 식이 a+b=a+b가 된다.

이제 refl, 을 입력하면 증명이 완료된다.

addition world, multiplication world...를 따라가면 교환법칙, 결합법칙, 분배법칙 등을 보일 수 있다. 여기는 평이하다.

개인적으로 Function world부터 혼란이 좀 있었는데, 각 tactic이 뭘 의미하는지 제대로 익히지 않고 뛰어들어서인 것 같다. 앞에 대충 따라가다가 갑자기 뒤에서 모든 개념이 섞여버렸다. 왼쪽에 각 tactic 설명이 자세히 나와있으니 읽으면서 하는 것이 좋다. 아니면 종이에 써 가면서 문제를 해결하거나? 머릿속으로만 하려다 보니 좀 어지러웠다. 

Function world는 논리와 집합 개념을 사용한다. 이와 관련된 내용을 설명하는 페이지https://leanprover.github.io/logic_and_proof/도 있다. 아직 읽는 중이다. 집합과 논리 과목을 직접 들은 적은 없다. 다른 전공책 1장에 나오는 Set Theory 이런 것은 좀 봤지만... 

 

그래서 Function world부터 무얼 하는 것이냐면... 예를 들어 명제 P, Q가 있고, 명제 Q를 보이고 싶다. 이를 P의 증명 p, P이면 Q이다의 증명 h가 있을 때, 명제 Q의 증명을 h(p)로 만드는 느낌? 해보면 안다.

 

내용을 간략하게 설명할 자신이 없어서 극히극히 일부만 언급했다. LEAN에 대해 궁금한 분은 직접 위에 있는 링크에 들어가서 The Natural Number Game을 순서대로 해결해나가길 바란다. 

그리고 LEAN을 본격적으로 공부하고 싶으면 https://leanprover.github.io/theorem_proving_in_lean/index.html을 읽어야 할 것 같다. 진행 예정...