그러고 보니 최근 재밌는 일이라고 생각한 게

[익명(sweater5651)]

https://arxiv.org/abs/2603.08139

물리 논문을 Lean으로  formalizing하다가 반례를 발견해서 수정했다고 하더라

처음에 저런 주제를 접했을 때 물리학과는 동떨어진 내용들이라고 봤는데 생각보다 요긴하게 쓰일 수 있을 것 같음

[익명(218.154)]

사실 어디까지 수학이고 어디까지 물리인지 잘 모르겠을 때가 있는데 증명기의 도움을 받을 수 있다는게 신기함

[익명(sweater5651)]

생각보다 반례가 간단해서 놀랐음. 컴퓨터 검증인지라 매우 복잡하고 괴랄한 반례일 줄 알았는데 저자들이 방심한 부분인 것 같기도 함

[익명(sweater5651)]

@ㅇㅇ 결론적으로 조건을 수정해서 증명하는데에 성공했으니 다행이지만 만약 명제 자체가 틀렸으면 인용수도 꽤 되어서 조금 참사였을지도

[익명(218.154)]

@ㅇㅇ 사실 그 부분이 현대 학계에서 제일 맹점이긴 하지 상호신뢰로 쌓아올려져있다 => 누군가의 실수가 묻혀있었다면 그 위로 쌓아올린 모든게 무너진다

[익명(218.154)]

@ㅇㅇ(218.154) 그렇다고 모든 과정을 검증해나가며 올라가기엔 시작조차 하기 어려워진다는 문제가 생기니 어디까지 내 머릿속에서 쌓아올리고 어디부터 사람들을 믿을지 이걸 조절하는 것도 참 힘든 것 같음. 나 요새 하는 거도 사람들이 다 가져다가 쓰는데 이걸 어디까지 신뢰해야할지 모르겠으니까 가끔 의구심이 듬. 이 사람들은 다 따라가보고 확신이 있어서 이렇게 쓰는건가?

[익명(sweater5651)]

@ㅇㅇ(218.154) 수학에서도 유한단순군 분류, 숄체의 Crystalline cohomology에 대한 이론도 그런 문제가 있어서 한번 엎어진 예시로 알고 있음

[익명(sweater5651)]

@ㅇㅇ(218.154) 한창 LLM 이용한 프리프린트가 많이 올라와서 어지럽던 때도 있었고 저번에 P=NP를 대수위상으로 해결했다고 주장한 프린트가 올라와서 봤는데 GitHub 링크로 가보니 아무것도 없고 배경만 주구장창 설명하다 증명은 스케치뿐이었던 경우를 봐서 여러모로 Formalizing을 자동화한다면 학계에 주는 영향이 클 것 같다고 생각함