쌓인 기록에서 찾기
무엇을 찾으세요? 날짜를 몰라도 됩니다. 제목·Key Point·요약·태그를 한꺼번에 뒤집니다.
검색 범위 2026년 8월 13일 (목) 부터 2026년 10월 30일 (금)까지 3636건
5건 · "Lean 4"조건 지우기 ×
001 00:11 ▲ 18 · 댓글 2 자동 정리 증명, 복잡한 워크플로우보다 단순 반복 루프가 더 효과적 형식 정리 증명(formal theorem proving) 분야는 계획, 분해, 전문 도구 연계 등 인간이 설계한 복잡한 워크플로우에 의존해왔으나, 비형식 수학은 대규모 언어 모델의 연쇄 추론으로 진전을 이뤄왔다. AI · 머신러닝 · h1: A Taste of the Bitter Lesson in Automated Theorem Proving
Key Point 자동화된 정리 증명에서 복잡한 설계 워크플로우 대신 단순한 에이전트 루프가 더 효과적일 수 있다는 발견은, 향후 형식 검증 시스템을 어떻게 구축할 것인지에 대한 근본적인 접근 방향을 바꿀 수 있다.
핵심 요약
형식 정리 증명(formal theorem proving) 분야는 계획, 분해, 전문 도구 연계 등 인간이 설계한 복잡한 워크플로우에 의존해왔으나, 비형식 수학은 대규모 언어 모델의 연쇄 추론으로 진전을 이뤄왔다. 이 논문은 '비터 레슨' 질문을 제기한다: 테스트 타임 계산을 확장하는 단순한 에이전트 루프가 이런 복잡한 워크플로우와 경쟁할 수 있는가? h1이라는 단순한 도구를 개발했는데, 이는 모델에게 Lean 4의 효율적인 인터페이스를 제공하고 검증자 피드백과 자기 성찰로 작동하며, 명시적 분해나 탐색 구조를 강요하지 않는다. 전체 요약 7문장 읽기 → 002 18:11 ▲ 114 · 댓글 22 수학 증명의 형식화, AI 자동화 시대 열리다 형식 증명은 수학의 기초와 논리 규칙 수준에서 철저히 검증한 증명으로, 컴퓨터로 자동 검사하는 것이 일반적이며 페르마 최종 정리·구 채움 문제 등이 형식화됐다. AI · 머신러닝 · What mathematicians should know about the Lean Theorem Prover: reliability & AI
Key Point AI가 수학 증명을 자동 형식화하기 시작하면서 신뢰성·일관성 검증의 새로운 시대가 열렸지만, 커널 버그와 AI 자체에 대한 신뢰 문제가 수학의 기초를 위협할 수 있다.
핵심 요약
형식 증명은 수학의 기초와 논리 규칙 수준에서 철저히 검증한 증명으로, 컴퓨터로 자동 검사하는 것이 일반적이며 페르마 최종 정리·구 채움 문제 등이 형식화됐다. 증명 보조기(proof assistant) 중 Lean이 수학자들에게 가장 인기 있으며, 2013년 Leo de Moura가 개발했고 마이크로소프트에서 오픈소스로 공개됐다. Lean의 표준 수학 라이브러리인 mathlib은 약 30만 개 정리, 10만 개 이상 정의, 250만 줄 코드로 700명 이상이 기여했다. 전체 요약 13문장 읽기 → 003 18:30 당일 +343 온톨로지 변경을 증명으로 검증하는 오픈소스 도구 프로덕션 온톨로지 변경을 계획·적용·롤백할 수 있으며, 영향 범위 보고서와 감사자가 검증 가능한 증명을 제공하는 Rust 기반 도구다. 오픈소스 · 도구 · fabio-rovai/open-ontologies · Rust
Key Point 온톨로지 변경의 모든 결과를 사전에 확인하고, 누구나 검증할 수 있는 증명을 함께 제공함으로써 프로덕션 환경에서의 신뢰성 문제를 근본적으로 해결하는 접근 방식이다.
핵심 요약
프로덕션 온톨로지 변경을 계획·적용·롤백할 수 있으며, 영향 범위 보고서와 감사자가 검증 가능한 증명을 제공하는 Rust 기반 도구다. 한 줄의 삼중항(triple) 변경이 901개의 새로운 결과를 만드는 경우, 텍스트 diff로는 볼 수 없는 의미론적 차이를 드러내는 형태 diff(shape diff) 보고서를 생성한다. 도구가 생성한 증명 파일(asserted.tsv, derivations.tsv)은 Lean 4 검증기로 검수할 수 있으며, 검증 명령어 oo-cert는 JVM 없이 독립적으로 실행 가능하다. 전체 요약 12문장 읽기 → 004 18:30 ▲ 115 · 댓글 53 11개 정사각형 최적 배치 증명, AI 보조로 완성 Lean 형식 검증을 통해 11개 정사각형의 최적 배치 문제에 대한 완전한 증명을 완성했다. AI · 머신러닝 · AI-assisted proof of optimal packing for 11 squares
Key Point 최적화 문제의 엄밀한 증명에 AI 보조 도구와 형식 검증이 어떻게 결합되는지 보여주는 사례로, 수학적 추측을 기계 검증 가능한 형태로 변환하는 최신 방법론을 시연한다.
핵심 요약
Lean 형식 검증을 통해 11개 정사각형의 최적 배치 문제에 대한 완전한 증명을 완성했다. 7,920개 지역 Lean 모듈을 EvolvingPrograms 검증 시스템으로 검증했으며 모든 감사에서 오류가 0건이다. 최적 한 변의 길이는 T = (6u+4)/(1+2u-u²) 형태이며, u는 방정식 5u⁸-10u⁷-2u⁶+14u⁵+12u⁴-6u³+2u²+2u-1=0의 (9/25, 37/100) 범위 내 유일한 근이다. 전체 요약 8문장 읽기 → 005 09:10 ▲ 125 · 댓글 121 OpenAI, Navier-Stokes 증명을 Lean 4 형식 증명으로 공개 OpenAI가 유체역학의 오랜 난제인 Navier-Stokes 방정식을 증명하면서 동시에 Lean 4 형식 증명을 공개했다. AI · 머신러닝 · OpenAI’s Navier-Stokes release included a Lean 4 formal proof
Key Point 형식 검증 비용이 만 배 절감되면서 AI 증명 방식이 학문과 산업 전반의 검증 방식을 근본적으로 바꿀 수 있는 전환점이 되었다.
핵심 요약
OpenAI가 유체역학의 오랜 난제인 Navier-Stokes 방정식을 증명하면서 동시에 Lean 4 형식 증명을 공개했다. 종전에는 수학 논문 한 페이지를 형식화하는 데 약 40시간이 소요되었으나, 이번 증명은 17시간 만에 Lean 형식으로 검증되었다. 166쪽 규모의 OpenAI 논문을 전통적 방식으로 형식화했다면 13만 2800인시가 필요했을 것으로 추정되어, 약 만 배의 비용 감소를 의미한다. 전체 요약 4문장 읽기 → 