# 350년 난제 '페르마의 마지막 정리' 컴퓨터 증명 나선 수학자들 > Clean Markdown view of GeekNews topic #14119. Use the original source for factual precision when an external source URL is present. ## Metadata - GeekNews HTML: [https://news.hada.io/topic?id=14119](https://news.hada.io/topic?id=14119) - GeekNews Markdown: [https://news.hada.io/topic/14119.md](https://news.hada.io/topic/14119.md) - Type: news - Author: [chabulhwi](https://news.hada.io/@chabulhwi) - Published: 2024-04-03T01:45:09+09:00 - Updated: 2024-04-03T01:45:09+09:00 - Original source: [dongascience.com](https://www.dongascience.com/news.php?idx=64615) - Points: 8 - Comments: 1 ## Topic Body ### 페르마의 마지막 정리, 컴퓨터 언어로 새로 증명한다 * [임피리얼 칼리지 런던][imperial]의 [케빈 버저드(Kevin Buzzard)][kbuzzard] 교수님이 2024년 10월부터 [페르마의 마지막 정리(FLT)][FLT]의 형식 증명을 [린(Lean) 정리 증명기][lean]로 작성할 예정입니다. * 영국의 [공학 및 물리 과학 연구 회의\[EPSRC\]][EPSRC]에서 버저드 교수님에게 연구비를 그달부터 5년 동안 지원하기로 했습니다. * [린 블루프린트(Lean blueprints)][blueprint]라는 [plasTeX][plasTeX] 플러그인을 이용해 만든 프로젝트 계획서가 2024년 4월 말에 공개될 예정입니다. #### 페르마의 마지막 정리는 이미 증명되지 않았나? 이미 증명됐습니다. 영국의 수학자 [앤드루 와일스][wiles]가 1994년에 증명을 공개했고, 이 증명은 1995년에 공식적으로 출간됐습니다. 하지만 [상호 작용 정리 증명기\[ITP\]][itp]의 언어로 작성된 [형식 증명][formal-proof]은 아직 없습니다. #### 상호 작용 정리 증명기? 형식 증명? 이게 뭐야? * [상호 작용 정리 증명기\[ITP\]][itp]: 사람이 형식 증명을 작성하도록 돕는 컴퓨터 프로그램. 증명 보조기[proof assistant]라고도 함. * [형식 증명][formal-proof]: 증명 검증기[proof verifier]라는 컴퓨터 프로그램으로 검증할 수 있는 증명. 증명 보조기는 대개 증명 검증기 역할도 함. #### 정리 증명기는 인공 지능인가? [신경 정리 증명기\[NTP\]][ntp]는 그렇다고 볼 수 있지만, 린을 비롯한 많은 상호 작용 정리 증명기는 기계 학습 기반의 프로그램이 아닙니다. #### [린(Lean) 정리 증명기][lean]를 소개해 줘. * 상호 작용 정리 증명기 겸 순수 함수형 프로그래밍 언어. * 의존 유형론에 기반을 둠. * 유형 클래스, 확장 가능한 구문, 매크로, 메타프로그래밍 등의 기능이 있음. * 다른 증명 보조기와 비교할 때, 린의 이용자층에는 [(수학 기초론 밖의 분야를 연구하는) 수학자가 *특히* 많음.][favorite] #### 페르마의 마지막 정리의 형식 증명은 왜 작성하려는 거야? 케빈 버저드 교수님이 [X에 올린 포스트][tweet]를 인용하자면, "컴퓨터로 하여금 현대 정수론을 이해시켜서, 결국에는 정수론자들을 도울 수 있게 하기 위함입니다." #### 링크 * 2023년 10월 3일에 케빈 버저드 교수님이 린 줄립(Zulip) 챗에 올린 메시지: https://leanprover.zulipchat.com/#narrow/stream/113486-announce/topic/Formalising.20Fermat/near/394513901 * 린 수학 라이브러리: https://github.com/leanprover-community/mathlib4 * 뉴사이언티스트 기사: https://institutions.newscientist.com/article/2422601-mathematicians-plan-computer-proof-of-fermats-last-theorem/ * 파퓰러메카닉스 기사: https://www.popularmechanics.com/science/math/a60280173/machines-are-on-the-verge-of-tackling-fermats-last-theorema-proof-that-once-defied-them/ [imperial]: https://www.imperial.ac.uk/a-z-research/number-theory/people/ [kbuzzard]: https://github.com/kbuzzard [FLT]: https://en.wikipedia.org/wiki/Fermat%27s_Last_Theorem [lean]: https://lean-lang.org/ [EPSRC]: https://www.ukri.org/councils/epsrc/ [blueprint]: https://github.com/PatrickMassot/leanblueprint [plasTeX]: https://github.com/plastex/plastex/ [wiles]: https://en.wikipedia.org/wiki/Andrew_Wiles [itp]: https://en.wikipedia.org/wiki/Proof_assistant [formal-proof]: https://en.wikipedia.org/wiki/Formal_proof [favorite]: https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/mathematicians'.20favorite.20proof.20assistant.3F/near/351505672 [ntp]: https://openai.com/research/formal-math [tweet]: https://twitter.com/XenaProject/status/1774027504711332078 ## Comments ### Comment 24184 - Author: calofmijuck - Created: 2024-04-03T10:02:41+09:00 - Points: 2 응원합니다. Formal proof에 관심이 있으신 분들은 Terrence Tao 교수님의 Machine Assisted Proofs (https://www.youtube.com/watch?v=AayZuuDDKP0) 강의 들어보시는 것도 추천드려요.