The QED manifesto was a proposal for a computer-based database of all mathematical knowledge, strictly formalized and with all proofs having been checked automatically.
A dedicated mailing list was created, and two scientific conferences on QED took place, the first one in 1994 at Argonne National Laboratories and the second in 1995 in Warsaw organized by the Mizar group.
In a 2007 paper, Freek Wiedijk identifies two reasons for the failure of the project.
[4] Similar projects include the Metamath proof database and the mathlib library written in Lean.
[5] In 2014 the Twenty years of the QED Manifesto[6] workshop was organized as part of the Vienna Summer of Logic.