이런 결과가 분산 컴퓨팅 같은 실제 분야에 응용될 수 있는지 궁금함. 아니면 순수 수학적인 흥미로만 존재하는 것인지 의문임
전혀 바보 같은 질문이 아님. 기술적 통찰이 분산 알고리즘이나 계산 복잡도 이론에서 새로운 불가능성 정리로 이어질 수도 있음. 메시 네트워킹 같은 응용 가능성도 흥미로움
“모든 현대 수학은 집합론 위에 세워졌다”는 말은 너무 단정적임. Lean이나 Rocq 같은 현대 수학 도구들은 형식화된 수학(formalized mathematics) 기반으로 발전 중이며, 이는 형식 이론(type theory) 위에 세워져 있음
나는 수학자는 아니지만, ZFC는 여전히 유효한 기초 체계라고 생각함. 종속형(dependent types) 은 정리 증명 관리에 유용하지만, 더 많은 정리를 증명하게 해주지는 않음. Lawrence Paulson의 Isabelle/HOL은 타입 기반이 아니지만 대부분의 수학을 증명할 수 있음
하지만 실제 수학자들은 형식화된 수학을 거의 사용하지 않음. 알고 있어도 불편함 때문에 기초 언어로 쓰지 않음
수학의 언어와 그 언어에 대해 증명하는 형식 언어를 혼동하면 안 됨. 전자는 거의 전적으로 집합을, 후자는 필연적으로 타입을 사용함
보다 정확히 말하면, 수학의 기초 위기는 집합론의 형식화로 일단락되었다고 보는 게 맞음
“cons’es all the way down”이라는 농담식 표현으로, 재귀적 구조를 풍자함
“드디어 무한을 계산할 수 있다”는 말에 감격함
다음 달 Bay Area에서 The Dillinger Escape Plan의 Calculating Infinity 투어가 열린다고 함. 공연 링크. 수학, 해킹, mathcore 팬층이 겹칠 것 같아 공유함
“무한을 계산한다”는 말에 “그리고 그 너머로!”라고 응답하며 농담을 이어감
Haskell에서는 let x = x in x 한 줄로 가산 무한(countable infinity) 을 표현할 수 있다고 함
“Chuck Norris가 1부터 무한까지 두 번 셌다”는 밈으로 유머를 덧붙임
“이건 정말 오래 걸렸음 /s”라며 풍자적 표현을 덧붙임
“컴퓨터 과학은 유한한 것만 다룬다”는 주장에 동의하지 않음. 실제로 컴퓨터 과학은 무한에 깊이 관여함
Quanta가 이런 식으로 다루는 건 흔한 일임. 대중 과학식 서술로 인물 중심 이야기에 집중하고, 세부 내용은 생략하는 경향이 있음
다만 컴퓨터 과학은 비가산 무한(uncountable infinity) 에는 관심이 적음. 측도론(measure theory) 은 주로 그쪽을 다룸
나도 처음엔 “CS는 무한을 근사한다”고 생각했지만, 실제로는 근사(approximation) 라는 말이 핵심임. 우리는 항상 유한한 경계 안에서만 일함. 우주가 무한하더라도 우리가 관측할 수 있는 범위는 빛의 속도로 제한됨
“컴퓨터 과학은 논리를 사용하지 않는다”는 식의 문장은 너무 게으른 표현임. Boolean 논리가 바로 그 증거임
나는 오랫동안 수학을 공부했는데, 무한(infinity) 은 존재하지 않는다고 믿게 되었음. 수학은 무한이 없을 때 더 나을 수도 있다고 생각함
나도 공학 수준의 수학만 배웠지만, 무한은 숫자가 아니라 과정(process) 이라고 생각함. {1, 2, 3, ...}의 “...”는 끝이 없는 확장 과정을 의미함. 무한번째 소수 같은 건 없고, 더 큰 소수가 항상 존재한다는 생성 규칙만 있을 뿐임
하지만 무한을 제거하면 수학이 끔찍하게 복잡해짐. 자연수를 끝없이 확장하지 않는다면 계산이 매우 불편해짐
수학은 존재 여부보다는 개념적 유용성에 관심이 있음. 원도 현실에 존재하지 않지만 유용함. 무한이 없다면 결국 “x가 매우 매우 큰 수로 갈 때의 극한” 같은 형태로 다시 발명해야 함
“8에서 멈추면 된다”는 농담으로 무한의 불필요함을 풍자함
무한은 끝나지 않는 과정을 가리키는 이름일 뿐임. 어떤 과정은 더 빠르게 증가하기 때문에 더 큰 무한이 존재함. 개인적으로는 Riemann 구 모델의 무한 개념을 좋아함
“node_modules”가 내 파일 시스템에 무한의 수학을 연결해놓았다는 농담으로, 의존성 폭증을 풍자함
“모든 현대 수학은 집합론 위에 세워졌다”는 문장에 반박하며, 형식 이론(Type Theory) 도 있다고 지적함
Hacker News 의견
이런 결과가 분산 컴퓨팅 같은 실제 분야에 응용될 수 있는지 궁금함. 아니면 순수 수학적인 흥미로만 존재하는 것인지 의문임
“모든 현대 수학은 집합론 위에 세워졌다”는 말은 너무 단정적임. Lean이나 Rocq 같은 현대 수학 도구들은 형식화된 수학(formalized mathematics) 기반으로 발전 중이며, 이는 형식 이론(type theory) 위에 세워져 있음
“cons’es all the way down”이라는 농담식 표현으로, 재귀적 구조를 풍자함
“드디어 무한을 계산할 수 있다”는 말에 감격함
let x = x in x한 줄로 가산 무한(countable infinity) 을 표현할 수 있다고 함“컴퓨터 과학은 유한한 것만 다룬다”는 주장에 동의하지 않음. 실제로 컴퓨터 과학은 무한에 깊이 관여함
나는 오랫동안 수학을 공부했는데, 무한(infinity) 은 존재하지 않는다고 믿게 되었음. 수학은 무한이 없을 때 더 나을 수도 있다고 생각함
“node_modules”가 내 파일 시스템에 무한의 수학을 연결해놓았다는 농담으로, 의존성 폭증을 풍자함
“모든 현대 수학은 집합론 위에 세워졌다”는 문장에 반박하며, 형식 이론(Type Theory) 도 있다고 지적함