Daily OSS

tag: Lean4 · 2건

학습 완료 OpenAI, AI 모델로 10년 이상 미해결 수학 난제 10개 풀었다고 주장
2026-08-01 · Simon Willison · 원문 ↗ #ai-llm#math-reasoning#lean4
  • 근거: AI/LLM이 수학 난제를 해결했다는 연구 성과 기사로, 실무 도구가 아닌 AI 능력 트렌드 해설에 해당
  • 액션: openai/ten-proofs 저장소를 훑어보며 Lean 4 형식화 증명이 어떻게 구성되어 있는지 살펴보기
학습 완료 AI가 생성한 60,000줄 Lean 증명으로 공식 검증된 3D CSG 메시 교차 연산
2026-07-28 · HN (show hn) · 원문 ↗ #formal-verification#ai-agent#lean4
  • 근거: AI 에이전트 활용한 형식 검증(Formal Verification) 실험 — AI/LLM 신뢰성 및 코드 검증 방법론 관점에서 흥미로운 사례
  • 액션: https://schildep.github.io/verified-3d-mesh-intersection/ 웹 데모 실행 후 README에서 93줄 spec과 AI 생성 증명 구조 훑어보기