Theorem.chat 에 대해
Theorem.chat은 수학적 주장을 받아들여 그것을 규정하려고 합니다. 당신은 주장을 밝히고, 그것이 만족해야 하는 기준을 명시합니다. AI 모델의 패널 - 당신이 원하는 만큼, 당신이 원하는 벤더에서 - 그것을 공격하고, 하나 더 많은 모델 심판. 그 다음에 논쟁은 Mathlib에 대항하여 Lean 4에서 공식화되고, 린 커널은 그것이 증명되었는지 여부를 결정합니다. 마지막 단계는 제품입니다.
다른 모델이 아닌 커널을 사용하는 이유
모델에게 어려운 질문을 던지면 옳은지 아닌지에 대한 유창한 답을 얻을 수 있습니다. 여러 명에게 질문하면 그들은 종종 동의합니다. 이는 확증처럼 느껴지지만 그렇지 않습니다. 모델은 훈련 데이터와 맹점을 공유합니다. 첫 번째를 검사하는 두 번째 모델은 여전히 같은 종류의 판단이며, 이것을 둘러볼 수 있습니다. 린 커널은 할 수 없습니다. 공리와 Mathlib에서 문장을 파생하거나, 그렇지 않으며, 자신감은 결과에 영향을 미치지 않습니다.
형식적인 증명을 위조하는 일반적인 방법은 검사되고 거부된다. sorry에 구멍을 남기는 증명, 커널이 신뢰에 대한 계산을 하게 만들기 위해 native_decide에 호소하는 증명, 또는 조용히 새로운 공리를 소개하는 증명은 성공으로 계산되지 않고 감지되고 거부된다.
패널이 실제로 할 수 있는 일
논쟁은 싸게 얻을 수 있는 부분입니다. 패널은 문헌을 사용합니다 — arXiv, OpenAlex, Crossref — 그래서 알려진 결과는 나쁘게 재파생되는 대신 인용됩니다. 그것은 계산을위한 SageMath과 PARI/GP, SMT 해결을위한 Z3와 CVC5, OEIS 검색을 위해 그것이 구축 한 시퀀스를 식별하고, 네트워크 액세스가 없는 샌드박스 파이썬 환경을 가지고 있습니다. 추측은 누군가가 그것을 증명하려고 노력하는 라운드를 보내기 전에 만 가지 사례에 대해 테스트 할 수 있으며, 반대 예제는 즉시 토론을 종료합니다.
증거, 웅변이 아닙니다
일치는 인수의 질에 따라 점수가 매겨지지 않습니다. 주장은 수락 기준으로 분해되며, 기준은 제 3 자가 그 뒤에 무언가를 다시 검사할 수 있을 때만 해결됩니다. 관련된 구절이 인용된 소스 또는 실제로 실행된 코드와 실제 출력이 있습니다. 심판은 판결하기 전에 그 증거 자체를 다시 검사합니다. 기준이 아직 열려 있을 때 일치가 끝났다고 선언할 수 없습니다.
너는 표준을 세웠지
표준은 선택할 수있는 당신의 것이며, 심판은 문자 그대로 그것을 보유하고 있습니다. 조심스러운 전문가가 수락 할 것인지 물어보십시오. 모든 가정이 명시 된 완전한 유추 논증을 요청하고 대신 그에 대해 판단을 받습니다. 상금 제출이 직면 할 바를 요청하고, 솔직한 결과는 일반적으로 패널이 어디에 짧은 떨어졌는지의 정확한 계정입니다 - 어쨌든 자신감있는 주장보다 더 가치가 있으며, 당신은 어쨌든 스스로 확인해야합니다.
명확히 말하자면, 이것은 열린 문제를 해결하는 기계가 아닙니다. 그것은 해결되지 않은 논증을 통과시키는 것을 거부하는 기계이며, 어떤 단계가 실패했는지 정확히 알려줍니다.
실패한 형식화는 유용한 출력입니다.
린이 증명을 닫지 않을 때, 여러분은 남아있는 정확한 목표를 얻게 됩니다. 실제로 그것은 거의 항상 비공식적인 논쟁이 손을 흔들었던 장소입니다. 모든 사람이 산문 버전을 읽고 머리를 끄덕였을 것입니다. 그 목표는 이미 시도한 것과 함께 공격하기에 가장 적합한 좌석에 전달되고, 다른 것은 없습니다. 모델은 막혀 있을 때 쓰러지고, 전체 비용으로 자신을 재정의합니다. 대신 특정 질문을 통과하면 일반적으로 토큰의 일부를 잠금 해제합니다.
오랜 작업이 살아남습니다
패널이 설정한 모든 리마는 증명과 함께 공유 대장에 들어가므로 결과는 한 번만 기록되고 다시 파생되지 않으며 막다른 골목은 기록되어 아무도 다시 돌아오지 않습니다. 일치는 서버 측에서 실행되며 예산, 공급업체 중단 또는 탭을 닫은 경우 깨끗하게 일시 중지되고 중단된 곳에서 정확히 재개됩니다.
이것은 무엇을 위해하지 않습니다
이 사이트는 수학, 논리, 이론 컴퓨터 과학, 이론 물리학 및 경제 이론을 위해 만들어졌습니다 - 주장이 증명에 의해 해결되는 분야. 생물학, 의학, 화학 또는 사회 과학에서 경험적 질문은 정리를 생성하지 않습니다, 그들은 발견을 생성하고, 어떤 양의 형식화는 그들을 결정하지 않습니다. 우리의 자매 사이트 referee.chat은 똑같은 패널과 심사원 프로세스를 실행합니다 린 단계없이, 정확히 그 질문에 대한.