Lean린
Lean은 수학적 증명과 프로그램의 성질을 코드로 표현하고 컴퓨터로 검증하는 정리 증명 도구이자 프로그래밍 언어다.
기사 2편
최근 언급 Lean은 Microsoft Research의 Leonardo de Moura가 2013년 개발을 시작한 오픈소스 정리 증명 도구(proof assistant, 증명을 컴퓨터로 검증하는 소프트웨어)이자 함수형 프로그래밍 언어다. 수학적 명제와 증명을 형식 언어로 작성하면 컴퓨터가 증명의 각 단계를 검증한다. 2023년부터는 비영리 조직 Lean FRO가 개발을 이끌고 있다.
수학 증명의 형식화와 소프트웨어 검증에 쓰이며, 공동체가 함께 만드는 수학 라이브러리 mathlib가 널리 쓰인다. AI 분야에서는 모델이 생성한 증명을 기계적으로 검증하는 수단으로도 쓰인다.
이 설명은 AIPOST 기사와 널리 알려진 사실을 바탕으로 정리했습니다. 잘못된 내용이 있으면 정정 요청으로 알려 주세요.
이 항목을 다룬 기사
두 사람은 Lean 코드 작성을 위해 ChatGPT의 Codex 도구를 사용한 것으로 알려졌습니다.