What kind of reference website does Lean4 still need?

Stream: general

[Daniel Donnelly]

Wouldn't it be great if we had a database of proofs viewable on the web? Do we already have that? Please link me. Will the stackexchange site have avenues for doing this kind of Q&A-style database of proofs? You should be able to click a button and everything for the most part loads into VSCode. How would you handle duplicates of proofs? Or is this a bad idea, because we already have it, though it takes some digging to find what you need...?

[Eric Wieser]

Are you aware of https://leanprover-community.github.io/mathlib_docs for Lean 3?

[Eric Wieser]

As for "click a button and load in vs-code", the "open in gitpod" button on the mathlib readme on GitHub basically does that - although you have to navigate to the corresponding file by hand

[Daniel Donnelly]

@Eric Wieser I'm aware of the docs now. However, where is a site for all the known Lean-verified proofs?

[Eric Wieser]

https://leanprover-community.github.io/lean_projects.html has a list of projects from the community that are not mathlib itself, if that's your question.

[Eric Wieser]

It's certainly not an exhaustive list