매스립
Lean 프로그래밍 언어를 위한 방대한 수학 라이브러리이다. 대수학, 해석학 등 다양한 수학적 개념과 정리들이 공식화되어 있어, LLM이 생성한 코드 속성을 증명할 때 필요한 수학적 근거를 제공한다.