코덱스 20계정 병렬 실행으로 Erdős 미해결 문제 27개 풀었다는 'Star Fleet' 프로젝트 등장

이 하네스가 정확히 어떻게 탐색하는 건지, Lean 증명 코퍼스는 어디서 가져온 건지, Ton 618 코드는 오픈소스인지 물어봄

이거 펀딩 누가 하는 거임? 이 정도 컴퓨팅 규모면 돈이 어마어마하게 들 것 같은데

검색해보니 개발자가 Xinobi AI라는 일본 스타트업 CTO더라

돈 있는 사람들이 사이드 프로젝트로 이런 거 하는 게 결국 서구 문명 만든 거 아니냐

컴퓨팅 파워랑 검색 하네스 자체는 진짜 흥미로운데, Fable이 쓴 증명 요약문이 사람이 이해하기 힘든 AI 말투라서 별로임. Erdős 문제 같은 게 가치 있는 이유는 새 기법을 낳기 때문인데 이런 식이면 그 의미가 줄어드는 느낌임

좋은 피드백 고마움, 사람이 읽기 편하게 리포트 개선해볼게

이거 딱 비디오게임에서 코인 모으는 거랑 똑같은 구조 아니냐, 코인은 장비 사는 데 쓰고 장비는 코인 더 모으려고 쓰는 거잖음

나도 AI로 수학 증명 실험해보고 싶었는데 컴퓨팅이 진짜 큰 걸림돌임. 이거 오픈소스 계획 있음?

이거 수학의 재미를 빼앗는 거 아니냐, 실질적 이득도 없는데 수학자들 일자리는 왜 위협하냐

수학자의 일은 증명을 만드는 게 아니라 수학을 연구하는 거임, 자동 증명기가 나온다고 수학자가 없어지는 건 아님. 엑셀 나왔다고 회계사가 없어진 게 아니잖음

나도 지난 3주 동안 거의 똑같은 걸 만들고 있었는데 마침 어제 평가 단계까지 왔음. 신규 증명 1개랑 첫 포멀화 13개 나왔음, 그래도 손으로 하는 수학이 더 좋긴 함

칭찬 고마움, 나도 첨단 AI로 새 수학 문제 푸는 게 신나긴 한데 손으로 하는 것도 여전히 좋아함

나는 ChatGPT 5.5한테 계속 더 풀어보라고 시키면서 Erdős 문제 붙잡고 있었음, Aristotle이라는 도구로 Lean 포멀화 시도 중임

Aristotle은 안 써봤는데 알려줘서 고맙고, 코드베이스도 탄탄해 보임

GPT를 자기 서버에서 돌린다는 게 무슨 소리임? OpenAI랑 특별한 계약 맺은 거임?

그냥 매번 다른 컨텍스트로 API 호출한 거지 모델을 직접 호스팅한 건 아닐 거임

GPT-5.6 instance라는 표현이 애매한데, 이거 클로즈드소스 모델인데 개인 프로젝트에서 어떻게 쓴 거임? API임 아니면 Codex임?

이거 어디 폴란드 포럼에서 답 그냥 복붙한 거 아니냐 ㅋㅋ

Lean 증명용 comparator 셋업 추가하면 신뢰도 확 올라갈 듯. AI가 Lean 컨텍스트를 몰래 조작해서 soundness를 깨지 않는지 확인하는 장치가 있어야 함