거의 세 주 전, 나는 전문 수학자와 아마추어 수학자, 자동 정리 증명 도구, AI 도구, 및 증명 보조 언어 Lean의 노력을 결합하는 협업 프로젝트를 제안했습니다. 이 프로젝트는 최대 네 번의 마그마 연산 호출을 사용하여 표현할 수 있는 마그마에 대한 4694개의 등식 법칙을 설명하는 추론 그래프를 묘사하는 것입니다. 즉, […]