[일반] 공리,규칙을 컴퓨터에 입력하고 모든조합을 찾으면 안되나요

[익명(125.143)]

컴퓨터의 무식한 연산력으로 모든 가능한 증명과 정리를

자동으로 만들수 없나요?

- dc official App

[Oo(118.235)]

공리까지 갈 것도 없이 랜덤하게 타자쳐서 반지의 제왕 같은 작품이 나올 가능성을 따져보면 되겠지. 반지의 제왕이 다 뭐야 동요 한 소절이라도 나올 가능성이 있을지 고민해 봐.

[익명(125.143)]

가능한 연결조합이 정해져있지 않나요 그냥 아무 문자열 늘어놓으면 수학적으로 말이안될수도 있잖아요 - dc App

[Oo(118.235)]

그 "가능한 연결조합"이란 게 몇 갠데? 그게 26개 넘으면 알파벳 무작위 나열하는 것과 복잡도 똑같은데?

[익명(125.143)]

@Oo(118.235) 공리가 그렇게 많나요 - dc App

[익명(112.148)]

ZFC 공리는 무한개래

[익명(125.143)]

ㄷㄷ - dc App

[익명(212.104)]

그것도 다 옛말이지

[익명(118.235)]

그 조합이 가산무한개인데 어떻게 함

[익명(106.255)]

그게 진심으로 된다고 생각하고 질문하냐

[익명(125.143)]

자동증명기 원리는 모르는데 이렇게 할거같아서요 - dc App

[ㅆㅅ(siiot)]

저 방법으로는 2+2=4 증명도 한 세월 걸릴 듯

[익명(223.38)]

원론적으로야 가능하지만 2가지 문제점 1. 의미있는 정리를 얻을 확률이 너무 낮음 2>1 3>1 4>1 5>2 6>3 이딴 정리들이 산더미처럼 그리고 다른 의미있는 정리들보다 훨씬 많이 나올것임 2. 그렇게 나온 정리의 과정과 결론을 알아볼 수가 없음 페아노 공리계의 공리만으로 소수의 무한성을 서술하고 증명한걸 누가 얼마나 알아볼까? 더 복잡한 정리들은? 그래서 증명보조기는 보통 1의 문제 때문에 결론에서부터 공리/증명된 정리로 환원하는 방식을 택하고 2의 문제 때문에 기초 공리계뿐만 아니라 충분히 사람이 이해할 수 있는 수준으로 서술된 정의와 정리들을 기호화해놓은걸 필요로 함 그럼에도 확률이 여전히 똥이기 때문에 brute force가 아닌 사람이 어떤 명제가 유효할 것 같다고 판단해야하기 때문에 '보조'

[익명(223.38)]

그리고 기호화나 유효성 판단 같은 인간의 역할을 llm으로 대체한게 '자동'

[익명(1.227)]

튜링머신이 님이 말한거랑 좀 비슷한 개념임. 함 찾아보셈

[익명(1.227)]

1928년. 당시 수학계를 이끌던 다비트 힐베르트 (David Hilbert) 는 다음과 같은 의문을 제시하였다. 수학자들이 지금까지 해 왔던 일들을 정리해보니 몇 가지 추론 법칙을 조합하여 원하는 결과를 도출하는 것이 전부임. 그렇다면 몇 개의 추론 규칙을 제시하면 앞으로 수학자들이 증명할 명제 또한 모두 찾을 수 있지 않을까? 즉, 모든 수리 명제를 자동으로 만들어 낼 날이 올 수도 있겠구나. 힐베르트는 이러한 보편 규칙이 존재하는가에 대한 의문을 제시했다. 하지만 3년 후 독일의 신참 수학자 쿠르트 괴텔이 이는 불가능한 일임을 증명해버렸다. “기계적인 방식만으로는 수학의 모든 사실을 구성할 수 없다.” 이를 불완전성의 정리 (incompleteness theorem) 라 한다.

[익명(1.227)]

https://horizon.kias.re.kr/19364/
여기
좀 잘 정리되어있는듯

[익명(symbol9756)]

테렌스 타오가 하고있음 magma 대수쪽으로 - dc App