오늘의 발명 실마리: 수학 증명할 때 인간의 언어 없애기
수학 증명할 때 식 중간에 사람의 언어로 적는데 이 부분까지 과학적 기호나 언어나 프로그래밍 언어로 대체할 수 있나? Coq란 수학 증명용 언어가 있는데 이게 그건가?