Palomar registers Lean proofs against a commit, and refuses to referee them

Palomar opened for submissions on August 18, offering mathematicians a public registry where a formal proof written in Lean can be tied to fixed source code, mechanically checked, and inspected long after the announcement that carried it has passed ^[1]. The load-bearing design decision is a refusal: Palomar registers what a repository snapshot proves and explicitly declines to referee the mathematics ^[7].

Terence Tao, the UCLA mathematician and 2006 Fields Medalist, announced the opening in a blog post ^[2]. He is one of four initial technical maintainers, alongside Matthew Ballard, Nestor Guillen, and Jaume de Dios Pont ^[3], and the project was incubated by the Lean Focused Research Organization and the Institute for Computer-Aided Reasoning in Mathematics ^[4]. Tao framed it as a response to a proliferation of AI-generated proofs, some of them formalized in Lean ^[5]. His stated problem is a reader-cost problem: without Lean expertise, checking one of these repositories is hard, because the proof has to typecheck, avoid unauthorized axioms, and formally state the same result being described in ordinary mathematical language ^[6].

The submission format is where the design shows. A registered entry is an external GitHub repository snapshot pinned to a specific commit ^[8], and it carries three files: a short Challenge.lean stating the claimed result, a Solution.lean module with the proof, and a formalization.yaml holding the informal description, metadata, and disclosures ^[9]. The mechanical check runs Comparator, a Lean tool that holds the advertised statement apart from the proof and asks whether the solution actually establishes the challenge ^[10]. Lean's documentation says Comparator supports theorem-statement matching and can call Lean's kernel and the independently implemented Nanoda checker ^[11]; the available materials do not establish that Palomar requires every one of those validation options ^[12]. The separation targets a specific failure mode: a repository can hold a perfectly valid proof of something other than the theorem being advertised outside the code ^[13].

The second check is not deterministic. According to Tao's announcement, a large language model judges whether the informal description in formalization.yaml appears to match the formal result and whether the repository meets the registry's minimum standards ^[14]. So of the two checks Palomar describes, one is reproducible and one is a sample from a model ^[21]. The project documentation itself warns that language-model review can miss discrepancies, and says readers still have to examine whether the definitions and the formal statement capture the theorem under discussion ^[15]. Palomar's published policy describes an automated registration review, and the supplied materials do not establish whether maintainers run separate human moderation ^[16]. Tao recommends human review at submission time and states that the checks fall well short of peer review for novelty, interest, and accuracy ^[17].

The boundary language is unusually disciplined for a launch. Registration certifies no novelty, no importance, no code quality, no correctness of an informal writeup; it does not mean an expert referee looked at the work, and it does not convert a GitHub repository into a journal publication ^[18]. Tao calls the thing a "zeroth approximation" of a preprint server for Lean proofs ^[7]. What survives is one narrow assertion: a proof from a named snapshot passed Palomar ^[22].

Two things worth tracking. First, whether the semantic bridge holds, since the informal-to-formal gap is exactly where the nondeterministic check sits ^[14][15]. Second, whether human moderation appears in policy rather than in recommendation ^[16][17]. The governance is broader than the four maintainers: the scientific advisory board includes Jeremy Avigad, Bryna Kra, Kim Morrison, Ravi Vakil, and Akshay Venkatesh ^[19]. The pattern is portable to any field drowning in machine output, provided that field has something as unforgiving as a typechecker to pin claims to.