HARD PROBLEMS · 2026.08–09 · STOPPED AFTER PRIOR-WORK CHECK
형식증명 패키지는 기계 검증을 통과하고 공개 DOI로 남았다. 그러나 같은 결론과 Lean 형식화가 먼저 존재한다는 사실을 확인해 출판 경로를 끝냈다.
2026년 8월, Ulrich의 u4가 양의 함의 논리의 단일 공리가 아님을 보이는 명시적 무한 반모형을 구성했다. Lean 커널 빌드, 별도 심볼릭 검사, 공리 감사와 소스 스캔을 거쳐 패키지를 고정했다.
검증한 것
기록된 빌드는 Lean 4.30.0에서 종료 코드 0으로 끝났다. 결정 파일에는 sorry, admit, 사용자 정의 공리나 우회 선언이 없었고, 독립 검사도 통과했다. 패키지는 2026년 8월 21일 공개 보존 기록으로 남았다.
늦게 확인한 것
공개 검색만으로는 같은 결과를 찾지 못했지만, 관련 연구자 확인에서 동일한 결론과 Lean 검증이 몇 달 먼저 존재했다는 사실이 드러났다. 9월 2일 저널 기록도 선행 결과 중복을 이유로 종료됐다. 결정문이나 비공개 메일은 공개하지 않는다.
기계는 증명 객체가 정해진 규칙을 통과했는지 확인했다. 그 결과가 새롭다는 것까지 확인해 주지는 않았다. 재사용 가능한 형식화는 남았지만, 최초 결과나 새 정리로 소개할 근거는 없다.
Project record
기간: 2026-08-21–09-02
활동: 무한 반모형 구성, Lean 형식화, 독립 검사와 공개 보존
내부 근거: 형식증명 소스, 검증 로그, 심볼릭 검사기, 해시와 범위 문서
외부 검증: 공개 Zenodo DOI와 CI 기록; 관련 연구자 확인과 저널 종료 기록
최종 결과: 형식검증 완료, 신규성 없음, 동료평가 출판 없음
공개하지 않은 것: 연구자·편집자 이름, 메일·결정문 원문, 제출 식별자