Lean4로 PBS Kids의 형식 검증

요약

이 게시물은 형식 검증 언어인 Lean4를 사용하여 PBS Kids의 Cyberchase 에피소드를 형식적으로 검증한 내용을 상세히 설명합니다. 저자는 원리로부터 수학적 원리를 도출하는 쇼의 초점에 영감을 받아, 이를 엄격한 검증이 필요한 소프트웨어 공학에 적용합니다. 이 글은 Lean에서 Nim의 변형인 에피소드의 게임을 모델링하고, 함수의 정의 방법, 적에 대한 비결정적 선택 처리 방법, Lean의 증명 전술을 사용하여 재귀 함수의 종료 증명을 보여줍니다. Lean이 수학적 사실을 표현하고 기본 공리까지 코드 동작을 검증하는 데 얼마나 강력한지 강조합니다.