Palomar Registry Launches as a Preprint Server for Lean‑Verified Mathematics

Palomar provides a lightweight, automated gatekeeper for Lean formalizations

Palomar는 Lean 코드를 포함하는 GitHub repository의 스냅샷을 수락하고, 공식적인 문장이 type‑check되는지 확인하며, 대규모 언어 모델을 사용하여 비공식적인 설명과 주장된 결과 사이를 비교하는 새로운 registry입니다. 기계적 확인(Lean 도구 Comparator 사용)은 논리적 정확성을 보장하는 반면, AI 확인은 비공식적인 주장에 대한 비결정론적 sanity test를 제공합니다. Palomar는 arXiv의 최소 수락 기준을 반영하여, 참신함이나 흥미에 대한 인간의 peer review를 명시적으로 수행하지 않습니다.

Submission workflow is intentionally rigorous yet achievable

제출 프로세스는 다음과 같이 구성됩니다:

정형화된 정리(theorem)에 대한 간결하고 사람이 읽을 수 있는 Lean 문장인 challenge file.
전체 Lean 증명을 포함하는 solution module.
비공식적인 설명, 메타데이터 및 공개 사항을 제공하는 formalization.yaml 파일.

Tao는 Sendov’s conjecture의 자신의 정형화된 증명을 성공적으로 등록함으로써 이 프로세스를 시연했습니다. 이 registry는 인간, AI agent, 또는 하이브리드로부터의 기여를 수락하며, 현대적인 AI assistant가 제출의 기계적 측면을 도울 수 있습니다.

Community reaction highlights strengths and concerns

"The second check (b) is non‑deterministic, being performed by a large language model. Shouldn’t this be just preliminary? I think submissions should have an additional, human‑performed level of verification." – Anonymous comment

"We do not have the resources to host and maintain repositories directly, but would be open to expanding the whitelist of approved repository hosting services beyond Github if there is sufficient demand for doing so." – Terence Tao

"A very quick look at Palomar suggests that it would be much more helpful if each submission required (a) a meaningful Title, and (b) a (well‑written) Abstract explaining what is proved — just as one sees in arXiv." – David Bevan

"Palomar will definitely be something we integrate for data checks and validation" – ygtisik (author of a registry of AI usage in science).

이러한 코멘트는 세 가지 반복되는 주제를 나타냅니다:

Verification depth – 일부 사용자는 자동화된 확인을 넘어선 인간의 검토 레이어를 원합니다.
Repository hosting – GitHub에 대한 의존성은 단일 실패 지점(single point of failure)으로 간주됩니다. 다른 forge로 확장하는 것이 바람직합니다.
Metadata quality – arXiv 관행과 유사하게, 더 명확한 제목과 초록(abstract)은 검색 가능성을 높여줄 것입니다.

Technical design choices and trade‑offs

GitHub‑centric model – identity, spam control, 및 versioning을 단순화하지만, 단일 서비스에 대한 의존성을 만듭니다. 여러 코멘터가 언급했듯이, 향후 확장 시 다른 git forge를 whitelist로 지정할 수 있습니다.
AI‑driven semantic check – 정형화된 문장과 비공식적인 설명 사이의 불일치를 표시하는 확장 가능한 방식을 제공하지만, 비결정론적입니다. Registry는 이를 확정적인 판단이 아닌 예비비로 취급합니다.
Minimal human involvement – arXiv의 방식을 반영하여, 전담 검토 팀 없이도 예상되는 Lean formalization의 양에 맞춰 시스템을 확장할 수 있게 합니다.

Why mathematicians might contribute

Visibility – 항목들이 검색 가능한 registry에 나타나며, 저자에게 크레딧을 제공하고 formalization을 더 넓은 커뮤니티에 노출합니다.
Reusability – 검증된 Lean 증명은 다른 프로젝트로 가져올 수 있으며, 이는 노력의 중복을 줄여줍니다.
AI ecosystem support – registry는 AI proof assistant를 훈련시키거나 평가할 수 있는 고품질의, 기계적으로 확인 가능한 데이터를 제공합니다.
Community standards – 참여함으로써 Lean formalization을 위한 best-practice 관행을 형성하는 데 도움을 줍니다.

Comparison with existing efforts

TheoremDB와 Metamath는 이미 정형화된 증명의 검색 가능한 데이터베이스를 제공하지만, Palomar는 Lean에 특화되어 있으며 자동화된 type-checking과 AI 기반의 semantic validation을 통합합니다.
Isabelle AFP는 Isabelle/HOL을 위한 오랜 archive를 제공합니다. Palomar는 아직 초기 단계이지만 Lean의 대응물로 볼 수 있습니다.

Outlook and open questions

Human‑level validation – 제3자 서비스가 Palomar의 최소 확인 절계를 위에 얹어 peer review를 수행할 수 있습니다.
Metadata enhancements – formalization.yaml에 명시적인 title과 abstract 필드를 추가하는 것은 항목들을 학술적 preprint-norm에 맞게 조정하는 것입니다.
Hosting diversification – GitHub를 넘어 확장하는 것은 단일 플랫폼에 대한 의존성을 완기화하고 다른 forge로의 사용자들을 수렴합니다.
Incentive structures – 커뮤니티는 명성이나 재사용 가능한 formalization에 대한 욕구 외에 무엇이 기기여를 동기부여하는지 여전히 탐색하고 있습니다.

Palomar is now open for submissions. Detailed instructions are available at the registry’s how‑to‑submit page, and discussion continues on the dedicated Lean Zulip channel.