수리논리에 모델론이라는게 있잖아
이게 형식화 즉,lean같은 증명보조기에 집어넣을 언어를 만드는데 필수적이지
컴퓨터가 이해할 언어로 만들려면 논리로 환원을 해야하는데
그럴려면 이산적인 수학구조를 만들 해석도구가 필요함
만약 새로운 혁명이 일어나면 연속적인 수학구조물도 이해할 뭔가가 만들어지겠지
최근에 필립 그리피스라는 기하학자가 호지관련 강연한걸 봤는데
대충 함수의 근을 찾아간 여정을 강연햇음
방정식을 만들거나 발견해서 복소수나 실수같은 수의 패턴을 찾아내서 다양체 즉,기하적인 구조물을 찾아냄
근데 이게 선형대수적인 측면과 미적분학적인 측면이 섞여있는
미분형식을 집중적으로 연구함
즉,대수기하 해석학이 듬뿍들어간 고난도 문제인거지
근데 만약 우리가 이걸 컴퓨터가 이해할 수 있는 논리식으로 표현할 방법을 찾으면 수학자 100명이 할 일을 하루만에 끝낼지도 모르지
알다시피 gpt도 결국은 확률모델로 돌리는건데
현재 알려진 바에 따르면 확률모델도 기하나 대수로 환원가능하다는 의견이 있음 타오가 자기 블로그에서 잘은 모르지만 에르고딕 이론을 대수랑 합치는게 가능하다고 함
지금 gpt 같은 확률 모델들은 가끔씩 존나 이상한 값을 도출하잖아 그걸 lean이랑 결합시켜서 해결하자는 논의도 나오는중
혹시 강연 링크좀 알ㄹ려주실수 있으신가요