집합론 대신 타입이론으로 기초 바꾸고... 를 말하기에는 내가 아직 타입 이론을 몰라서 말하기가 좀 그럼. 그래도 타입 추론 규칙이면 나쁘지 않을 듯? 그런데 추론 규칙 가르친다 해도 연계가 안 되어서 쓸데없이 배우는 양만 늘어날 것 같음. 그리고 타입이론으로 기초를 바꾸면 극한을 어떻게 다루느냐도 잘 모르겠음.


그런데 Theorem Proving in Lean 4 해보니까 3-4장은 할 만하고 수학의 정석보다 훨씬 나음.


그래서 학생들이 교과과정 중에 한 번쯤 해보는 건 나쁘지 않다고 생각함.