14

Proposal: Proof assistants

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

3
  • 6
    Do the OP of such questions really want them moved? If they are existing questions then it seems that they will not be moved. (ref).
    – Guy Coder
    Nov 20, 2021 at 17:54
  • 1
    Thanks for the reference! @GuyCoder
    – ice1000
    Nov 20, 2021 at 21:32
  • Many (answered) questions on existing sites are a good indicator that the new site is not necessary. Proposals covering scopes that no existing site covers are more likely to succeed (and result in a healthy site).
    – Raphael
    Jan 17, 2022 at 11:41

3 Answers 3

Reset to default
17

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

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

On SE CS, there are also plenty of them:

We also have questions about designing and implementing proof assistants.

On SE TCS (pretty much the same tags):

1
  • Note that some questions with these tags might refer to programming with dependent types rather than using them for theorem proving, so they would not strictly fall under "proof assistants".
    – Jesper
    Nov 20, 2021 at 14:53
-1

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.

2
  • Then someone wants to copy answers from one site to the next. Later others feel that they should have s specialized site and so copy the Q&A again. Where does it end?
    – Guy Coder
    Dec 9, 2021 at 21:33
  • @GuyCoder: I agree. A new question on this site is of course better! But when quickly establishing a new site (in which I have no experience of), cloning existing stuff (with attribution) may be a half-way solution (which matches your comment to the OP "If they are existing questions then it seems that they will not be moved").
    – jeq
    Dec 9, 2021 at 22:03

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .