qedbot

Registries

Where the registries disagree

Other projects record AI mathematics too. qed.bot reads 1059 of their entries and joins them only on keys a source supplies — never on similar titles.

125results 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 simply 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
318 entries read
vibemathed
741 entries read
placed
153 join to something held here
unplaced
906 name no problem this register holds. This register is anchored on curated problem lists; the others cover results across mathematics.
only here
365 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 any automated ingest can be. A disagreement recorded here is a prompt to look, not a verdict, and the raw labels beside each position show where two projects simply cut their scales differently.

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