Daniel Donnelly (Jan 17 2022 at 22:38):
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 (Jan 17 2022 at 23:12):
Are you aware of https://leanprover-community.github.io/mathlib_docs for Lean 3?
Eric Wieser (Jan 17 2022 at 23:13):
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 (Jan 17 2022 at 23:15):
@Eric Wieser I'm aware of the docs now. However, where is a site for all the known Lean-verified proofs?
Eric Wieser (Jan 17 2022 at 23:19):
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 (Jan 17 2022 at 23:20):
It's certainly not an exhaustive list
Last updated: Aug 03 2023 at 10:10 UTC