qedbot

Formal record

The formal record

What 567 Lean projects declare about their own proofs, set against what an independent check has actually established.

249 checked by Palomar 316 with no independent check 0 contradicted Check history ↓ Overview ↓

Browse declarations

Filters

Check history

52 checks

Every check attached to a result: rebuilt here, registered by Palomar, or tested by the object checker.

Erdős Problem 501

elliotglazer/erdos501/tree/218d1c1e46f77d4db80e566d1721782e85b94a17

Registered by Palomar at 218d1c1e: Comparator confirmed 7 theorems prove the recorded statement within Palomar's axiom policy, replayed through Lean's kernel and the independent nanoda kernel. The project names this problem, which does not establish that it proves the result claimed here, so it is not counted as a check of it

verified Palomar 7 theorems
Erdős 684

jidodat/erdos684-lean/tree/4543ff7764f9e8f1b2732a8464d5c19c945bfc52

Registered by Palomar at 4543ff77: Comparator confirmed 5 theorems prove the recorded statement within Palomar's axiom policy, replayed through Lean's kernel and the independent nanoda kernel. The project names this problem, which does not establish that it proves the result claimed here, so it is not counted as a check of it

verified Palomar 5 theorems
Erdős 190

jbaelaw/erdos190-lean/tree/be43a3ead08a9d9af352cf296d284dd3468ca805

Registered by Palomar at be43a3ea: Comparator confirmed 4 theorems prove the recorded statement within Palomar's axiom policy, replayed through Lean's kernel and the independent nanoda kernel. The project names this problem, which does not establish that it proves the result claimed here, so it is not counted as a check of it

verified Palomar 4 theorems
Erdős Problem 266

benkeene/erdos266/tree/aa0cd43fb45d4f8a3019bf8925424c06b1e67874

Registered by Palomar at aa0cd43f: Comparator confirmed 2 theorems prove the recorded statement within Palomar's axiom policy, replayed through Lean's kernel and the independent nanoda kernel. The project names this problem, which does not establish that it proves the result claimed here, so it is not counted as a check of it

verified Palomar 2 theorems
Erdős 625

SamPetkov/Erdos625-formalization/tree/9702b5e734627e3fdaef8da0d65ad7394016f0a7

Registered by Palomar at 9702b5e7: Comparator confirmed 2 theorems prove the recorded statement within Palomar's axiom policy, replayed through Lean's kernel and the independent nanoda kernel. The project names this problem, which does not establish that it proves the result claimed here, so it is not counted as a check of it

verified Palomar 2 theorems

Overview

567declarations read
249checked by Palomar
316checked by nobody independent
348reviewed by their authors or not at all
19assume results from the literature
0contradicted by a rebuild
About the index

A Lean project can publish a formalization.yaml declaring what it proves, which axioms its results rest on, what it assumes from the literature, how the work was produced and who reviewed it. This register reads every one it can find, across 348 repositories.

A declaration is not evidence. A check is: this register rebuilds proofs and objects itself, and cites Palomar, which rebuilds a project at a pinned commit, confirms with Comparator that the proof proves the recorded statement, and replays it through two independent kernels. Where a declaration and a check disagree, the disagreement is the finding.

Copies kept under review, verification and history directories are set aside before anything is read, and only the newest version of a versioned result is kept: 142 snapshot copies and 11 superseded versions this build. 38 declarations join a statement or record held here.

What a verdict means
verified
Elaborated, and every theorem rests on the standard axioms alone — or, for Palomar, registered after Comparator and two kernels accepted it.
axioms
Elaborated, but something further is assumed — typically the native_decide pair, which trusts the compiler rather than the kernel.
incomplete
A theorem depends on sorryAx, so an unproved goal survived into the final term.
fragment
The file imports its own project's modules, so it is a statement or a fragment rather than a standalone proof.
no deps
The project's dependencies could not be resolved at the pinned commit.
invalid
An object failed the constraints of its own problem.
refuted
An object is sound but does not reach the value claimed for it.
Fidelity grades
F3
Anchored. The proof is checked for exact statement identity against a statement written independently of it, held here from a separate statement corpus.
F2
Declared. The authors record how the formal statement corresponds to the claim — a comparator challenge, an alignment table or written divergences — or a statement corpus cites the proof against its own statement.
F1
Unaudited. A formal artifact exists, but nothing records that its statement says what the claim says.
F0
None. No formal statement is attached to the result.