[ok123456]

It tends to invent whole fake packages.

[dunham]

Yup, I got some nice documentation (minor syntax error) for a Http package in Lean that doesn't exist. I asked about Lean4 and it helpfully explained that the non-existent package had moved from Lean to Std.