# 테렌스 타오의 Proof Checkers 및 AI 프로그램에 대한 견해

> Clean Markdown view of GeekNews topic #15325. Use the original source for factual precision when an external source URL is present.

## Metadata

- GeekNews HTML: [https://news.hada.io/topic?id=15325](https://news.hada.io/topic?id=15325)
- GeekNews Markdown: [https://news.hada.io/topic/15325.md](https://news.hada.io/topic/15325.md)
- Type: GN+
- Author: [neo](https://news.hada.io/@neo)
- Published: 2024-06-13T16:33:19+09:00
- Updated: 2024-06-13T16:33:19+09:00
- Original source: [scientificamerican.com](https://www.scientificamerican.com/article/ai-will-become-mathematicians-co-pilot/)
- Points: 1
- Comments: 1

## Topic Body

### AI가 수학자들의 '공동 파일럿'이 될 것임

#### 수학의 변화

- 수학은 전통적으로 고독한 학문이었음.
- 최근에는 수학의 많은 부분이 개별 구성 요소로 엄격하게 분해되어 컴퓨터로 검증 가능해짐.
- UCLA의 테렌스 타오는 이러한 방법들이 수학에서 새로운 협력 가능성을 열어준다고 믿음.

#### 자동 증명 검사기의 등장

- 자동 증명 검사기를 통해 수학자들이 수백 명과 협력할 수 있게 됨.
- 예를 들어, 타오는 Polynomial Freiman-Ruzsa (PFR) 추측을 20명 이상과 협력하여 증명했음.
- 각 개인이 작은 단계의 증명을 기여하고, 전체 방향을 관리하는 방식으로 진행됨.

#### 수학의 형식화

- 모든 사람이 프로그래머일 필요는 없고, 수학적 방향에 집중하는 사람과 형식적 증명을 만드는 사람으로 역할을 나눌 수 있음.
- 표준 수학 라이브러리의 개발로 형식 수학이 실용적으로 변함.
- Lean이라는 프로젝트는 기본적인 수학 정리를 포함한 방대한 라이브러리를 가지고 있음.

#### AI와 수학의 미래

- AI가 수학자들의 보조 역할을 할 가능성이 있음.
- AI가 증명을 형식화하고, 논문을 작성하여 제출하는 등의 작업을 도울 수 있음.
- 인간이 아이디어를 제공하고, AI가 이를 형식화하는 방식으로 협력할 수 있음.

#### 수학의 새로운 방식

- AI와 협력하여 수학의 새로운 방식이 등장할 가능성이 있음.
- 수학자들이 프로젝트 매니저처럼 역할을 나누고, AI가 증명을 돕는 방식으로 변화할 수 있음.
- 수학 교과서를 형식화하여 더 상호작용적인 학습 도구를 만들 수 있음.

#### AI의 한계와 가능성

- AI가 수학의 큰 문제를 해결하는 데 도움을 줄 수 있지만, 인간의 직관과 이해가 여전히 중요함.
- AI가 제공하는 증명을 인간이 분석하고 이해하는 새로운 유형의 수학자가 필요할 수 있음.
- AI가 수학의 새로운 영역을 탐구하고, 인간이 이해하기 어려운 부분을 도울 수 있음.

#### GN⁺의 의견

- **AI의 역할**: AI는 수학자들이 더 큰 문제를 해결하는 데 도움을 줄 수 있는 도구로서 중요한 역할을 할 수 있음.
- **협력의 중요성**: AI와 인간의 협력은 수학의 새로운 가능성을 열어줄 수 있음.
- **형식화의 필요성**: 수학의 형식화는 더 많은 지식을 명시적으로 만들고, 협력을 촉진할 수 있음.
- **미래의 수학자**: AI와 협력하여 증명을 분석하고 이해하는 새로운 유형의 수학자가 필요할 수 있음.
- **기술 발전**: AI와 수학의 결합은 기술 발전에 따라 더 많은 가능성을 열어줄 수 있음.

## Comments



### Comment 26237

- Author: neo
- Created: 2024-06-13T16:33:20+09:00
- Points: 1

###### [Hacker News 의견](https://news.ycombinator.com/item?id=40646909) 
- **Edsger Dijkstra의 글**: 소프트웨어 생산 방식을 풍자한 1975년의 글을 언급하며, 지적 재산권에 대한 비판이 주된 내용임.

- **LLMs의 능력**: 현재는 도우미 역할을 하지만, 앞으로는 더 높은 수준의 통찰을 제공할 가능성이 있음. 예를 들어, 핵폭탄과 퇴비 더미의 관계를 이해하는 것처럼 인간이 놓치는 부분을 포착할 수 있음.

- **인터뷰 요약**:
  - **프로젝트 매니저 수학자**: AI와 증명 보조 도구가 수학적 통찰을 생산하는 데 혁신적일 수 있음.
  - **암묵적 지식**: 직관과 실패의 지식이 논문에 포함되지 않기 때문에, 수학자들 간의 소통이 중요함.
  - **수학의 형식화**: 증명 보조 도구가 이해를 돕기 위해 수학을 더 형식화할 필요가 있음.

- **컴퓨터 검증 증명**: AI가 체스 엔진처럼 증명 검증에 유용할 수 있음. 많은 정리와 보조 정리를 다루는 데 어려움이 있지만, AI가 이를 개선할 수 있음.

- **소프트웨어 역사와 수학**: 과거의 소프트웨어 프로젝트와 현재의 모듈화된 소프트웨어 엔지니어링을 비교하며, 수학도 비슷한 길을 갈 수 있다는 의견.

- **Terence Tao의 강연**: 수학 연구에 Lean을 사용하는 방법에 대해 더 자세히 설명한 강연을 추천함.

- **GPT-4를 사용한 수학 증명**: GPT-4가 새로운 보조 정리를 증명하는 데 성공한 사례를 소개함. 이는 수학 연구에 유용할 수 있음.

- **초기 경력 수학자와 Lean**: 초기 경력 수학자들은 직관을 신뢰하고 논문을 작성하는 것이 더 나을 수 있다는 의견.

- **실패로부터 배우기**: 다른 사람의 실패로부터 배우는 것이 매우 생산적이라는 의견.