qedbot

The formal record

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

285 checked by Palomar 349 with no independent check 0 contradicted Check history Overview

Browse declarations

Filters
Checked by: Anyone or nobody
Review: Any review
Method: Any method
Declares: Anything

Check history

56 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
Erdős 1220

jbaelaw/erdos1220-lean/tree/9cb81ffa48ffb766127c7e485ccef77bd4160868

Registered by Palomar at 9cb81ffa: 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 809

plasma-ai/erdos-809/tree/0f27743fabd97b262d2fce7946de9f0b3325a625

Registered by Palomar at 0f27743f: Comparator confirmed 1 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 1 theorems
Erdős 1219

jbaelaw/erdos1219-lean/tree/00e696a9cd2bbd8cad33d2cdc90ad385058c1466

Registered by Palomar at 00e696a9: Comparator confirmed 1 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 1 theorems

Overview

636declarations read
285checked by Palomar
349checked by nobody independent
389reviewed by their authors or not at all
23assume 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 400 repositories.

A declaration records what a project's authors say about their work; a check is a rebuild by someone else. 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. A declaration that a check disagrees with is marked contradicted.

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 16 superseded versions this build. 45 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
Absent. No formal statement is attached to the result.