Palomar Database

The public, machine-readable registry of Lean-verified mathematical results. This repository contains data, its schema, and data-integrity CI only. Intake, mechanical verification, editorial policy, review automation, and presentation live in the other Palomar repositories.

Stable interface

• index.json is the discovery endpoint.
• entries/PALOMAR-YYYY-MM-DD-NNNNNN-vN.json contains one immutable accepted version.
• schema-vN.json is the JSON Schema for entries declaring schema_version: N. The current one is schema-v1.json.
• renders/PALOMAR-YYYY-MM-DD-NNNNNN-vN/<sha256>/ contains that entry's immutable, content-addressed, browser-confined Challenge rendering.
• evidence/PALOMAR-YYYY-MM-DD-NNNNNN-vN/<sha256>/ contains that entry's immutable, content-addressed mechanical report and normalized workflow provenance.
• The GitHub Pages deployment publishes feed.xml plus per-subject feeds at feeds/arxiv/<category>.xml and feeds/msc/<code>.xml. Feeds contain the current version of each permanent result and rebuild on database updates.

Published entry, render, and verification-evidence files are append-only, byte for byte, and a published schema never changes meaning. Every (PALOMAR-YYYY-MM-DD-NNNNNN, version) pair is therefore an immutable record. Corrections and dependency updates make a new version; they never rewrite the source commit or verification record of an existing version. docs/append-only.md states the invariant exactly and describes how CI enforces it.

Versions intentionally do not promise mathematical or bibliographic continuity. A later version may change any substantive field, including the theorem, title, source, authors, or subject. A citation that needs stable meaning must name an explicit version, such as PALOMAR-2026-07-29-000001-v1. An unversioned identifier means the current/latest record and may change meaning when another version is published. In the permanent identifier, the ISO date is the acceptance date and the final numeric part is the originating issue number in PalomarRegistry/PalomarSubmission.

palomar-indexed Challenge dependencies are withdrawn. Schemas v2 through v5 are published and immutable, so they still name the value; schema v6 drops it, and validation rejects it in every schema version. No published record uses it.

Consumers should reject schema versions they do not understand and should use the commit-pinned source.tree_url, not a repository's moving default branch. Every record carries the pinned NanoDa commit used for the independent kernel replay; Palomar has no single-kernel record format.

Schema v6 records are backed only by mechanical report v3. source.project_path is absent for the natural repository-root layout and otherwise names the selected Lean project as a canonical repository-root-relative POSIX path. source.tree_url links directly to that selected directory; its path segments use RFC 3986 percent encoding. All formalization.*_path values remain repository-root-relative, so consumers should build file URLs from source.repository_url plus source.commit, not by appending them to source.tree_url. Challenge, Solution, Comparator configuration, and Lakefile paths stay inside the selected project. The metadata path may remain at repository root for a nested Comparator workspace.

Path-form formalization.project_dependencies also use normalized repository-root-relative paths, with . denoting repository root. The repository's one conventional root licence remains the recorded licence boundary for nested projects.

Mechanical report v3 supplies the exact fields bound by durable evidence: source.project_path, challenge.path, solution.path, comparator.path, formalization.path, and lakefile.path. Report v2 evidence continues to back schema-v5 records and is never promoted to schema v6 by inference. The current and proposed isolation boundary for browser render bundles is recorded in docs/render-origin.md.

Licensing

To make the registry easy to mirror and build on, the database metadata is released under CC0 1.0. Schema-v5 and later records bind the submitted repository's root licence path, SHA-256 digest, declared identifier, and mechanically detected SPDX identifier to its pinned commit. That evidence covers only the submitted repository snapshot; cited papers, reused formalizations, and dependencies keep their own licences.