What questions on existing SE sites are on proof assistants?

Question

Proposal: Proof assistants

I also wonder if these questions should be migrated to the new site if it's created successfully?

Answer 1

I believe searching by tags on StackOverflow already shows a looot:

• https://stackoverflow.com/questions/tagged/agda
• https://stackoverflow.com/questions/tagged/idris
• https://stackoverflow.com/questions/tagged/coq
• https://stackoverflow.com/questions/tagged/isabelle
• https://stackoverflow.com/questions/tagged/theorem-proving

The above tags are strictly about proof assistants, but mostly using them.

On SE CS, there are also plenty of them:

• https://cs.stackexchange.com/questions/tagged/agda
• https://cs.stackexchange.com/questions/tagged/type-theory
• https://cs.stackexchange.com/questions/tagged/dependent-types
• https://cs.stackexchange.com/questions/tagged/coq

We also have questions about designing and implementing proof assistants.

On SE TCS (pretty much the same tags):

• https://cstheory.stackexchange.com/questions/tagged/type-theory
• https://cstheory.stackexchange.com/questions/tagged/dependent-types
• https://cstheory.stackexchange.com/questions/tagged/coq
• https://cstheory.stackexchange.com/questions/tagged/agda

Answer 2

To add to your answer, there are quite a few on Math.SE:

• https://math.stackexchange.com/search?q=proof+assistant
• https://math.stackexchange.com/questions/tagged/automated-theorem-proving
• https://math.stackexchange.com/questions/tagged/theorem-provers
• https://math.stackexchange.com/questions/tagged/computer-assisted-proofs

and MathOverflow:

• https://mathoverflow.net/search?q=proof+assistant
• https://mathoverflow.net/questions/tagged/proof-assistants
• https://mathoverflow.net/questions/tagged/formalization
• https://mathoverflow.net/questions/tagged/coq
• https://mathoverflow.net/questions/tagged/formal-proof

Some of those tags are slightly abused / not specific to proof assistants, so one has to sift through them.

Answer 3

Instead of migrating questions, which would be unfair both to the OP and to the originating site, we could simply clone them by CC BY-SA 3.0. For example, we could repost https://mathoverflow.net/questions/240085/how-much-mathematics-has-been-formally-verified on this site proof[-]assistants as:

Editorial comment: This question has been copied from https://mathoverflow.net/questions/240085/how-much-mathematics-has-been-formally-verified, with the OP being Dan Piponi, dated May 2016, with 37 upvotes. Please note that any answers and comments from there have not been copied.

Title: How much mathematics has been formally verified?

That's a vague question so allow me to tighten it up a bit.

I recently noticed that there is a formal machine verified proof of the Central Limit Theorem (CLT) implemented with Isabelle. This requires a substantial amount of machinery that is taught in undergraduate courses on calculus, measure theory and probability theory. As Williams' textbook Probability with Martingales culminates with CLT it seems like it might be fair to conservatively estimate that maybe half of an undergraduate level probability theory course has been formalised.

So would it be fair to say that half of the material (in general) that is taught to mathematics undergraduates has been formally verified by machine? If not, what similar proposition is true?

And in the original question, one could add a link to the clone as a comment, or as an edit to the original question. And regarding reputation, the copy could be made community wiki, or the re-poster could be unregistered.