챗지피티로 검색하다가 알게 된 건데

[독두꺼비(testify6965)]

HOTT가 의외로 훨씬 많이 쓰인다고 함

보통 무한을 다루는 게 기존의 ZFC로는 한계가 있잖슴

그래서 보통 ZFC에 거대 기수를 추가하거나 범주론의 접근으로 무한의 크기를 비교하는데 여기서 가장 최근에 주목받는 게 HOTT라네

[요운(kk6062)]

많이 쓰이는진 모르겠는데 카테고리는 일단 많이 쓰이고있고 /// 그 많이 쓰이는거랑 무관하게 카테고리의 최신이론이 HoTT니까 그렇게 말한거 아닐지 (✖╹◡╹✖)◞

[독두꺼비(testify6965)]

coq였나 몇가지가 있던데

[독두꺼비(testify6965)]

무한의 크기를 계속 확장한다고 할 때 처리하는 알고리즘에서 테크닉적 어려움이 몇개 있기는 하지만 범주론에서 좀 더 계산적으로 나아간 거 같아서 좀 놀람

[Landau(hard4137)]

@독두꺼비 HoTT 자체는 이론이지 구현체가 아니다보니 "어디서" HoTT를 하느냐가 따로 있어야하는데 제가 아는 한 가장 빠르게 서포트한건 Coq이긴 함

[독두꺼비(testify6965)]

많이 쓰인다는 용례를 어떻게 이해한 건진 모르겠지만 글에서 말했을 때는 생각보다 HOTT가 활용되는 맥락이 꽤 있는 거 같다는 의미로 했던 말이었음 솔직히 이전에는 보예보츠키가 마틴뢰프의 논리를 확장했다 이 정도로만 생각했어서

[Landau(hard4137)]

전 사실 HoTT는 커녕 Curry-Howard 대응성 자체를 가끔씩 쿨 돌면 맛보기로 들춰보긴 하는데 도통 이해가 안가서 오래 고통받았었음

[Landau(hard4137)]

이게 자기 분야 아니면 자꾸 시간을 애매하게 쓰니까 이해를 애매하게 하는데 사실 이해를 못한거라 고통받는데, 수리논리 쪽은 애초에 자기 분야이기가 힘드니.. 근데 이제는 좀 알 것 같기도 함

[독두꺼비(testify6965)]

@Landau 오오 ㄷㄷ 눈을 떴구나

[Landau(hard4137)]

근데 저는 large cardinal쪽은 아예 안해보긴 함

[독두꺼비(testify6965)]

일단 거대 기수가 하도 종류가 많아서 우딘이 i0였나? 진짜 강한 버전으로 증명했지만 그거까지는 학계에서 필수적 공리로 받아들이지는 않는 분위기라고 함

[독두꺼비(testify6965)]

@독두꺼비 근데 가장 근본적으로 제일 약한 단계의 카디널은 그로센딕 유니버스랑 엮여서 알제브라 지오메트리에 필수적인 뒷받침이 되니깐 자명하든 유용하든 좀 인정하는 것처럼 보였슴

[Landau(hard4137)]

@독두꺼비 "논리적으로" large set의 문제는 categorification에 중요하고 그로센딕 유니버스도 그 일환으로 나온 개념이지만 생각보다는? 사람들 그다지 파운데이션에 관심없음. QFT 파운데이션에 물리학자들이 관심 없듯이 카테고리 이론하시는 분들도 파운데이션 잘 안함

[독두꺼비(testify6965)]

@Landau 아항 ㄷㄷ AGI에 수학하는 사람들 간다고 하는 줄 알았는데 카테고리 이론을 하는 사람들이 관심 안 가진다고 하는 건 의외네

[Landau(hard4137)]

예를 들어 모듈라이를 제가 결코 잘 알지 못한다만(뭐 꼭 그런게 아니더라도) diffeomorphism group같이 좀 어떻게 다뤄볼 엄두가 안나는 아주 큰, 무한 차원의 무언가를 다룰 때 사실 애초에 그런 큰거 쓸모조차 없으면 괜히 건드리고 싶지도 않을듯 지금은 자꾸 아웃풋이 나오니까 하는거지

[Landau(hard4137)]

@Landau 근데 아무튼 무한차원 리 그룹, 무한차원 벡터번들 같은걸 논할 때 1. 그것이 정확히 무엇을 말하는가? 이렇게 논리적인 궁금증이 떠오르는건 당연하지만, 사실 파운데이션 자체보다는 물리학자들이 이미 다루던 방식에서 힌트를 얻을 수 있음. 그 양반들은 대충 유한차원에서 되던 계산법들이 맞을거라고 치지

[Landau(hard4137)]

@Landau 그러면 좀더 refined된 질문은 2. 그것은 "얼마나" 혹은 "어떤 의미에서" 만만한 매니폴드와 유사한가? 이 문제를 따지고 나서 1번 문제를 다시 보면 3. 그런 성질이 필요하다면 그것의 정의는 무엇이어야 하는가? 1번은 사실을 묻는 것 같지만 사실 3번은 우리가 원하는 것, 필요한 것, 당위같은게 뭔지를 물어보는 뉘앙스가 됨 그러면 algebraic한 성향이 강한 사람들은 결국 이런 성질들을 보장해주기 위해 누군가가 똥치워주기를 바라며 기다려야하는데 가령 TVS(topological vector space)를 잘 다뤄야한다 이러면 좀 보기 싫더라도 다시 함수해석적 작업도 해야하고 그런거지

[독두꺼비(testify6965)]

@Landau 아 TVS 같은 걸 다룰 때 함수해석에서 다시 정의하는 작업이 뒷바탕이 돼야 되는 거라 그런 거임?

[Landau(hard4137)]

@독두꺼비 ㅇㅇ이렇게 사람들이 좀 필수적으로 필요성을 느끼고 어쨌든 수학이긴 하니까 팩트를 말해야하니까 "어쩔 수 없이" 다루는 재미없는 빌드업들이 있는데 그닥 공부하고 싶을만큼 흥미를 느끼진 못할 수도 있을듯 하물며 TVS가 아니라 large cardinals면 맥락에서 멀어지는만큼 인기는 떨어질 수 있음. 설령 그게 "논리적으로는" 필요하더라도

[독두꺼비(testify6965)]

@Landau 저번에 그로센딕이 대수기하로 빠질 때 당시 상황이 함수해석이 포텐이 너무 넘쳐서 그랬다고 들었는데 어쩌다가 다시 돌아가야 되는 거구나

[독두꺼비(testify6965)]

@Landau 님이 보시기에 많고 많은 어려움 중 결정적인 키포인트는 뭐라고 봄? 굳이 1개 꼽자면

[Landau(hard4137)]

@독두꺼비 "관심도가 떨어짐"이 중요한 이슈라고 봄여 저는

[독두꺼비(testify6965)]

@Landau 테크닉적 어려움이 아니고 걍 관심 부족이 문제였노

[Landau(hard4137)]

@독두꺼비 사람들이 애초에 ZFC를 엄청 중요시할지도 이제는 의문이라 ㅋㅋ

[독두꺼비(testify6965)]

@Landau ㅇㅇ 솔직히 ZFC는 비유하자면 물리에서 지금 시점에 상대성이론을 다루는 느낌

[Landau(hard4137)]

@독두꺼비 카테고리 이론의 개쩌는 새로운 아이디어가 ZFC에서 서포트 안되면 아마도 사람들은 그 아이디어를 성립시키는 파운데이션을 찾는데 ZFC 버리는건 일도 아닐 것 같은 느낌임 그로센딕 유니버스는 운좋게도 ZFC를 "확장하는" 파운데이션이었을뿐

[독두꺼비(testify6965)]

@Landau 교수님들 말하는 거 보면 오히려 ZFC가 역으로 어떤 시스템의 일부로 잡아먹힐 느낌이 들기는 함