ARCHIVE · 아카이브
Hard Problems · 난제와 탐구
-
CPU로 두루마리 표면을 찾으려 했지만, 읽은 글자는 0이었다
Vesuvius CT에서 CPU로 표면을 찾고 펼치는 코드를 구성했지만, 2026년 8월 18일 확인한 새 잉크와 글자는 0이었다. 입력 목록과 실행 결과를 대조하며 보존되지 않은 통과 표시를 바로잡았다.
-
A CPU pipeline for scroll surfaces, with zero characters read
My CPU attempt aimed to locate scroll surfaces and flatten CT data, but confirmed new ink and characters were zero on 18 August 2026. Missing raw outputs led…
-
기계 검증은 통과했지만 새롭지는 않았다
Ulrich u4의 무한 반모형을 형식화하고 Lean 4.33.0 강화판을 공개했다. 이후 같은 핵심 결과의 3월 선행 공개를 확인해, 2026년 9월 2일 저널 경로를 종료했다.
-
Machine-checked, but not new
I published a strengthened Lean 4.33.0 formalization of an infinite countermodel for Ulrich’s u4. An earlier public principal result led me to close the journal path on 2…
-
P2624의 증명 파일 일곱 개를 다시 만들었다
P2624의 공개 사양에서 증명 트리 일곱 개를 다시 만들었다. 점유 벡터와 정렬 규칙을 맞추고, 299,903,736개 노드와 파일별 해시를 비교한 2026년 8월 20일 재구성 과정.
-
Rebuilding P2624’s seven proof files
I rebuilt seven P2624 proof trees from the public specification, matching 299,903,736 nodes and all seven file hashes. The 20 August 2026 reconstruction depended on recovering the catalogue…