Lean으로 형식화한 유한 단순군 분류
Axiom Math가 유한 단순군 분류의 1세대 증명을 Lean으로 완전히 형식화했다고 발표했습니다. 형식화 과정에서 불균형 군 정리의 기존 증명에 문제가 있음을 발견해 대안 증명을 제시했고, Lean 커널이 각 논리 단계를 검사합니다.
개발·오픈소스 · 최신기사
개발 도구와 언어, 웹 기술과 오픈소스 프로젝트의 변화를 다룹니다.
OpenAI의 네이비어-스톡스 증명, 처음 알려진 접근과 달랐다
OpenAI의 Navier-Stokes 증명은 스페인 수학자들의 접근법을 그대로 따른 결과가 아니라, 세부 구조가 다른 방법을 사용한 것으로 전문가들이 파악하고 있습니다. 다만 대규모 LLM이 만든 Lean 증명과 논문 설명의 차이, 모델의 추론 경로를 확인하기 어려운 점은 남아 있습니다.
테렌스 타오의 ‘수학 2.0’ — 증명 풍요의 시대에 수학이 나아갈 길
테렌스 타오는 AI가 수학 문제의 증명을 빠르게 내놓는 ‘증명 풍요’ 시대에 문제 풀이만을 연구 목표로 삼으면 수학의 장기적 발전을 해칠 수 있다고 주장합니다. AI를 증명 생성에만 쓰기보다 인간의 이해와 새로운 연구 영역을 넓히는 데 활용하고, 평가 기준과 연구 관행도 바꿔야 한다고 제안합니다.
수학자가 Lean 정리 증명기에 알아야 할 것: 신뢰성과 AI
Thomas Hales는 Lean을 이용한 수학 형식화와 AI 자동 형식화의 진전을 소개하고, 증명 커널의 soundness bug와 Lean 형식 체계의 미해결 기초 문제를 짚습니다. 형식 검증 결과를 신뢰하려면 커널만 확인할 게 아니라 정리와 정의가 원래 의도와 일치하는지도 사람이 감사해야 한다고 강조합니다.
번역 과정에서 어긋난 나비에–스토크스 증명
이 논문은 자연어 수학 증명을 Lean으로 옮긴 뒤 검증해도 원래 증명이 충실하게 번역됐다는 보장은 없다고 설명합니다. 저자들은 의미를 보존하며 자연어의 모호성을 해소하는 일이 계산 복잡도 계층에서 정지 문제보다도 높은 수준에 이를 수 있다고 주장하고, OpenAI의 나비에–스토크스 증명에서도 두 표현이 맞지 않는 사례를 제시합니다.
AI가 만든 수학 연구 결과와 공개 방식
OpenAI가 내부 모델로 얻은 수학 결과를 GitHub에 공개하고, 일부 증명은 Lean 형식화 자료로 제공합니다. 추론 요약과 계산량 추정치도 공개했지만, Hacker News에서는 결과 검증과 수학계의 연구 관행을 둘러싼 논쟁이 이어집니다.
OpenAI Dots 에이전트 군집으로 47년 된 수학 하한을 높이다 — Lean으로 증명 검증
작성자는 OpenAI Dots의 에이전트 7개를 약 3일간 운용해 덮개수 문제 C(24,14,4)의 하한을 19에서 20으로 높였다고 보고합니다. 여러 에이전트의 교차 검토와 Lean 기계 검증을 거쳤지만, 수학자의 동료 검토는 아직 진행 중입니다.
애도할 것인가, 말 것인가?
수학 연구에서 AI가 어려운 문제를 풀기 시작하자 수학자들이 느끼는 상실감과 기대를 살핍니다. 저자는 수학의 가치를 ‘이해’ 하나로 설명하기 어렵다고 짚으며, 정리 증명·이론 구축·추측 제시를 나눠 AI의 현재 능력과 한계를 논하고 OpenAI에 비공개 수학 결과를 공개하라고 촉구합니다.
Factorio 품질 생산 계산하기
Factorio: Space Age의 품질 생산과 재활용 과정을 행렬과 선형 방정식으로 모델링하고, 장기 생산량을 정확히 계산하는 방법을 설명합니다. 저자는 계산을 자동화한 웹 도구와 소스 코드도 공개했습니다.
깊이로 나누면 즉시 3D가 됩니다
3D 카메라의 원리를 x와 y를 깊이 z로 나누는 원근 투영에서 출발해 설명합니다. 단순한 나눗셈이 perspective projection matrix와 전체 그래픽 파이프라인의 한 단계라는 점을 수식과 인터랙티브 예제로 보여줍니다.
인터랙티브용 새로운 등적 지도 투영법 — 줌인하면 Mercator로 자연스럽게 전환
저자 Ben Joffe가 전체 축소 상태에서는 등적(equal-area)이고 확대할수록 Mercator로 매끄럽게 전환되는 새 지도 투영법을 공개했습니다. atanh(sin(φ)·a)/a라는 단순한 폐형식 수식 하나로 순방향·역방향 변환과 줌 전환이 모두 처리되며, UN의 'Correct the Map' 결의 이후 Equal Earth 대안 논의에 실용적 선택지를 제시합니다.