Zulip Chat Archive

Stream: general

Topic: What kind of reference website does Lean4 still need?

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