qedbot

Where the registries disagree

Other projects also record AI results in mathematics. qed.bot reads 1132 of their entries and joins each to its own records by an identifier the source supplies, such as a problem number or the file a proof lives in.

128results held by more than one registry
40disagreements about who did the work
61where another registry holds stronger evidence
1cited proof repositories with no Lean

Disagreements about who did the work

40
Erdős 1039

erdos:1039

qed.bot: machine-led (A1/V2, A3/V1)·Entry

vibemathed: joint (their label: ai-co-developed)·Entry

autonomy
Erdős 1177

erdos:1177

qed.bot: joint (A1/V0)·Entry

vibemathed: machine-led (their label: ai-discovered)·Entry

autonomy
Erdős 451

erdos:451

qed.bot: joint (A1/V2)·Entry

vibemathed: machine-led (their label: ai-discovered)·Entry

autonomy
Erdős 514

erdos:514

qed.bot: joint (A1/V1, A1/V2)·Entry

vibemathed: machine-led (their label: ai-discovered)·Entry

autonomy
Erdős 610

erdos:610

qed.bot: joint (A1/V2)·Entry

vibemathed: machine-led (their label: ai-discovered)·Entry

autonomy
Erdős 696

erdos:696

qed.bot: joint (A1/V2)·Entry

vibemathed: machine-led (their label: ai-discovered)·Entry

autonomy
Erdős 866

erdos:866

qed.bot: joint (A1/V2)·Entry

vibemathed: machine-led (their label: ai-discovered)·Entry

autonomy
Erdős 953

erdos:953

qed.bot: joint (A1/V1)·Entry

vibemathed: machine-led (their label: ai-discovered)·Entry

autonomy
Erdős 1153

erdos:1153

qed.bot: joint (A1/V1)·Entry

vibemathed: machine-led (their label: ai-discovered)·Entry

autonomy
Erdős 1195

erdos:1195

qed.bot: joint (A1/V1)·Entry

vibemathed: machine-led (their label: ai-discovered)·Entry

autonomy
Erdős 380

erdos:380

qed.bot: joint (A1/V1)·Entry

vibemathed: machine-led (their label: ai-discovered)·Entry

autonomy
Erdős 603

erdos:603

qed.bot: joint (A1/V1)·Entry

vibemathed: machine-led (their label: ai-discovered)·Entry

autonomy
Erdős Problem 865

erdos:865

qed.bot: joint (A1/V3)·Entry

vibemathed: joint (their label: ai-co-developed)·Entry

vibemathed: machine-led (their label: ai-discovered)·Entry

autonomy
Erdős 870

erdos:870

qed.bot: joint (A1/V0)·Entry

vibemathed: machine-led (their label: ai-discovered)·Entry

autonomy
Erdős 896

erdos:896

qed.bot: joint (A1/V1)·Entry

vibemathed: machine-led (their label: ai-discovered)·Entry

autonomy

Proofs worth fetching

6

Another registry records a proof this one has not rebuilt. Each repository is first asked whether it contains any Lean at all.

How to read this

Three kinds of finding
disagreement
Two registries place the same result differently on who did the mathematics. Autonomy has no ordering, so this is a difference of judgement, and neither side is corrected here.
gap
One registry holds stronger evidence than another. The evidence ladder is ordered, so one of them knows something the other does not.
lead
Another registry names a proof for a result this one has not checked: a repository worth fetching rather than an opinion.
Coverage
palomar
377 entries read
vibemathed
755 entries read
placed
159 join to something held here
unplaced
973 name no problem this register holds. This register is anchored on curated problem lists; the others cover results across mathematics.
only here
373 results carrying AI claims here appear in no other registry read.
we hold more
10 results where this register holds stronger evidence.
What this is not

It is not an audit of anyone else's work. The registries that curate by hand are more careful per entry than an automated reading can be. A disagreement recorded here is a reason to look again, and the raw labels beside each position show where two projects divide their scales differently.

1 of the 6 repositories cited as holding a machine-checked proof contain no Lean sources at all.