[일반] lean, mathlib <--- 이거 전공자들은 어떻게 생각함?

[거북이이(turtl)]

소프트웨어관데 이거 보고 수학과로 편입하는거 괜찮아보임?

아직 한국에선 하는 사람 없다고 들었는데

[ㅆㅅ(siiot)]

ai 관련으로 못 엮으면 굶어죽음

[거북이이(turtl)]

그래도 해볼만한가... 아님 아무도 안 하는덴 이유가 있는건가...

[수갤러 1(121.152)]

하는 사람이 적은거지 있기는 함 그리고 세계적으로 유망하기는 한데 한국에서는 아직 잘 모르겠음

[거북이이(turtl)]

그렇구만... 하고싶다

[수갤러 1(121.152)]

@거북이이 국내 풀이 진짜 좁아서 시작해보면 다들 환영해줄거임

[거북이이(turtl)]

[수갤러 2(223.49)]

HoTT도 하거라

[거북이이(turtl)]

어흐 배울거 많다...

[익명(118.235)]

컴파일러쪽에 AST 가지고 Coq로 형식증명을 해서 코드안정성을 검증해보자는 시도가 있는건 봤는데 대부분 알지도 못하는거 보면 아직 수학 내부에서만 관심있어보임

[거북이이(turtl)]

음... 완벽히 이해했어...