수학계는 Lean 에 갇혀 있는가? 대안적 증명 보조기구의 가능성

Are We Stuck with Lean?

Lean 의 압도적인 인기는 필연적인 결과라기보다 몇몇 유명 수학자들의 선택에 기인한 사회적 현상일 수 있습니다. AI 기술의 발전으로 다른 증명 보조기구에도 대규모 라이브러리를 구축할 가능성이 열렸으며, Metamath 와 같은 대안을 통해 더 높은 정확성과 집합 이론 기반의 대안을 확보하는 것이 수학계에 유익할 수 있다고 제안합니다.