쌓인 기록에서 찾기
무엇을 찾으세요?
날짜를 몰라도 됩니다. 제목·Key Point·요약·태그를 한꺼번에 뒤집니다.
검색 범위부터 2026년 10월 30일 (금)까지3636건
6건 · "증명 보조기"조건 지우기 ×
001▲ 129 · 댓글 44Lean, 검증된 증명 커널 네 개 추가Lean v4.35.0부터 lake check 명령으로 개발 환경을 leanchecker(공식 커널)로 재검증할 수 있으며, 프로세스는 샌드박스에서 실행된다.AI · 머신러닝 · Lean now ships with verified kernels
Key PointLean 증명 보조기의 핵심인 커널에 버그가 증명을 검증하지 못하는 치명적 문제를 여러 커널로 재검증해 해결하는 방식이 도입되었고, 특히 형식적으로 증명된 Lean 기반 커널의 등장으로 신뢰성이 크게 강화되는 시점이다.
핵심 요약
- Lean v4.35.0부터 lake check 명령으로 개발 환경을 leanchecker(공식 커널)로 재검증할 수 있으며, 프로세스는 샌드박스에서 실행된다.
- nanoda, lean4lean, con-leche, con-ron 네 개의 추가 커널을 탑재했고, lake check --paranoid로 모든 커널로 증명을 재검증할 수 있다.
- con-leche는 Lean으로 작성되고 일관성이 증명된 첫 번째 커널이며, Claude(Fable과 Opus)가 구현하고 Joachim Breitner가 감독했다.
전체 요약 11문장 읽기 →AI · 머신러닝 · Simons Foundation launches $15M effort to help mathematicians navigate AI era
Key Point수학 분야의 AI 활용이 가속화되는 시점에 주요 재단과 AI 기업들이 연구자 커뮤니티를 지원하는 대규모 투자를 시작했으며, 이는 향후 수학 연구의 방향과 AI 도구 도입 기준에 실질적 영향을 미칠 것이다.
핵심 요약
- 시몬스 재단, Anthropic, OpenAI가 협력하여 수학 분야의 AI 전환을 지원하기 위해 총 1500만 달러를 투자하기로 발표했다.
- 이 자금은 개방형 공모를 통해 워크숍과 이니셔티브를 지원하며, 연구자들이 AI 보조 결과를 평가하고 새로운 도구를 배우며 AI 사용 기준을 정립하도록 돕는다.
- Anthropic과 OpenAI는 수학 분야를 넘어 기초 과학까지 AI 도구와 컴퓨팅 자원을 제공한다.
전체 요약 7문장 읽기 →AI · 머신러닝 · What mathematicians should know about the Lean Theorem Prover: reliability & AI
Key PointAI가 수학 증명을 자동 형식화하기 시작하면서 신뢰성·일관성 검증의 새로운 시대가 열렸지만, 커널 버그와 AI 자체에 대한 신뢰 문제가 수학의 기초를 위협할 수 있다.
핵심 요약
- 형식 증명은 수학의 기초와 논리 규칙 수준에서 철저히 검증한 증명으로, 컴퓨터로 자동 검사하는 것이 일반적이며 페르마 최종 정리·구 채움 문제 등이 형식화됐다.
- 증명 보조기(proof assistant) 중 Lean이 수학자들에게 가장 인기 있으며, 2013년 Leo de Moura가 개발했고 마이크로소프트에서 오픈소스로 공개됐다.
- Lean의 표준 수학 라이브러리인 mathlib은 약 30만 개 정리, 10만 개 이상 정의, 250만 줄 코드로 700명 이상이 기여했다.
전체 요약 13문장 읽기 →AI · 머신러닝 · The Future of Mathematics
Key PointAI가 수학 논문 수준의 결과를 생성하기 시작하면서 '수학이란 무엇인가'라는 근본적 질문이 제기되고 있으며, 수학의 본질은 문제 해결이 아니라 엄밀한 추론과 창의적 사고에 있다는 답변이 학문의 미래를 결정할 것이기 때문이다.
핵심 요약
- 수학 커뮤니티는 AI의 등장으로 근본적인 변화를 맞고 있다. 최근 몇 개월간 AI가 푼 개방형 문제들은 1년 전이라면 훌륭한 논문의 자료가 되었을 정도의 결과물이지만, 이제는 쉽게 생성되고 있다.
- 그러나 수학의 본질은 엄밀한 추론과 의사소통의 문화이며, 이는 수천 년간 변함없이 유지돼 온 핵심이다. AI 시대에도 수학적 사고가 필요하다는 점은 변하지 않는다.
- 현재 기초 모델(foundation model)의 특징은 전체 수학 문헌을 학습했으며 피곤함이 없다는 것이다. AI의 해법들은 기존 기법을 조합해 푸는 문제들이 대부분이며, 근본적인 통찰력이나 새로운 아이디어를 요구하는 문제는 여전히 풀기 어렵다.
전체 요약 14문장 읽기 →오픈소스 · 도구 · Anatomy of a Lean proof for software engineers
Key Point형식 증명은 프로그램처럼 작성되어 컴파일되므로, 이 사례는 소프트웨어 엔지니어가 타입 검사와 증명 보조기의 관계를 이해하고 실제 이론 문제에 어떻게 적용하는지 구체적으로 배울 수 있다.
핵심 요약
- 소프트웨어 엔지니어 입장에서 형식 증명이 무엇인지 이해하기 위해 Lean을 이용해 결정적 유한 오토마타(DFA) 이론 문제를 증명한 과정을 설명한다.
- 계산 이론 교재의 문제: 세 행의 비트 문자열(최상단 + 중간 = 최하단)에서 덧셈이 성립하는지 검증하는 언어 B가 정규언어임을 증명하는 것이었다.
- 정규언어의 폐쇄성을 이용해 B의 역순 B^R을 인식하는 DFA를 구성하면, B^R이 정규이므로 그 역순인 B도 정규임을 결론 낼 수 있다.
전체 요약 13문장 읽기 →기타 · What I did at Recurse Center
Key Point프로그래밍 집중 프로그램에서 LLM·알고리즘·언어학을 넘나들며 정말 만든 것들을 보려면 참가자들이 실제 무엇을 만들었는지 구체적으로 알아야 한다.
핵심 요약
- Recurse Center는 뉴욕 브루클린의 프로그래밍 집중 프로그램으로, 저자는 여름 배치에서 다양한 스터디 그룹과 프로젝트에 참여했다.
- Agentic Adventures 그룹에서는 LLM과 에이전트를 주제로 원격 샌드박스 구축, 'Just One' 게임 제작, minGPT 실습 등을 진행했다.
- Practical Deep Learning 스터디 그룹을 통해 Jeremy Howard의 책을 함께 읽으며 고전 머신러닝부터 신경망 구축까지 학습했다.
전체 요약 13문장 읽기 →