Highest scored questions
79 questions
23
votes
1
answer
249
views
Vote Early, Vote Often
It would be hard to over-emphasise how critical voting is for the health of an SE site. Voting is how good content gets recognized, wrong or incoherent content is signalled, and how a class of editors,...
- 101
17
votes
3
answers
323
views
Are SE "power users" trying to seed the site with "interesting questions"?
Excuse my ignorance about how things work, but looking at these questions
Could proof assistants be used to prove that some piece of code is free of bugs?
Which programming languages are most similar ...
- 11k
16
votes
0
answers
241
views
Announcing a once in a life time badge! (The Beta badge!)
In case you missed the announcement: participating in the private beta stage will give you a chance to receive a badge that is only obtainable within a limited time frame. This is called the Beta ...
15
votes
1
answer
120
views
Low-quality tags
There are some tags that I don't think are really necessary. They look like someone wanted to come up with more tags that would apply to their question and just lifted some words from the question; ...
- 3,270
15
votes
0
answers
252
views
Leaving Private Beta & Initial Pro-Tem Moderator Election!
Congratulations! You've met the participation and engagement expectations for an active private beta site and will be going into public beta tomorrow!
As we’re getting ready to wrap up the private ...
- 101
14
votes
1
answer
160
views
2022 Community Moderator Election Results
Moderator election #1 on Proof Assistants has come to a close, the votes have been tallied, and the new moderators are:
They will be your initial pro-tem moderator team — please thank them for ...
- 101
13
votes
2
answers
185
views
Is this for assistants only, excluding automated provers?
Do automated theorem provers fall under the scope of this new Stack Exchange sub-site, as well as Proof Assistants?
- 519
13
votes
1
answer
620
views
How are we doing in beta?
Beta sites do not automatically make it to a full site. There are requirements we have to meet.
See: What should the criteria be for Stack Exchange sites to leave beta?
Where can one see how the users ...
- 2,856
12
votes
2
answers
237
views
Syntax highlighting for proof assistants
In my answer to the question about the "Hello World" of proof assistants, the code is very monochromatic:
...
- 1,175
12
votes
0
answers
176
views
Ways to participate
It looks like the site has gotten off to good start, with a lot of interesting questions and answers! I just want to remind people of some of the other ways to participate that will help the site to ...
- 215
11
votes
9
answers
403
views
What should the name of our main chatroom be?
Every Stack Exchange site (Not all) main chatroom has a unique name that is related to the main site itself.
For example:
Super User: Root Access
Gaming: The Bridge
IoT: Chat of Things
Unix & ...
11
votes
1
answer
67
views
Should there be a mathlib tag for Lean?
There are already a number of questions that are specifically about the monolithic math library mathlib created in Lean. Should we have these kinds of tags ...
- 373
10
votes
3
answers
467
views
Candidate changes in 2022 Moderator Election – review your ballot
TL;DR: There's been a change in the candidate list for the 2022 Moderator Election. If you've already voted, you should confirm your votes still accurately represent your preferences. Details follow.
...
- 101
9
votes
1
answer
69
views
Does [theorem-proving] need to exist?
I think the theorem-proving tag should be deleted, because it is too general - almost every question will be related to theorem proving. Should it be deleted?
- 238
9
votes
2
answers
208
views
Enabling syntax highlighting of Lean and Coq
This follows on from Syntax highlighting for proof assistants, which establishes that it would be nice to have syntax highlighting, but incorrectly concludes that the ball is not in StackExchange's ...
- 971
8
votes
3
answers
114
views
Should questions arising from computational logic be asked?
When the site was proposed the name Proof Assistants was given (ref). However in the unofficial chat room, Area 51 meta questions and other places it became clear ...
- 2,856
8
votes
2
answers
190
views
Administrators and Permissions
Are there administrators?
If so, who are they?
If not, how will they be elected?
Will the permissions and roles be updated?
UPDATES:
15th March 2022 - Leaving Private Beta & Initial Pro-Tem ...
- 1,348
7
votes
4
answers
169
views
Policy on self-answers
Stack Exchange has a lot of general guidance on how to use the site, including how to ask and answer questions. One of those concerns the topic of self-answering questions (or more specifically, ...
- 1,088
7
votes
2
answers
136
views
User Abusing the System for Homework Problem?
I witness a user, called "learner123", posting similar questions on Stackoverflow and ProofAssistants Stackexchange, then suddenly all his questions are "voluntarily removed". See:
...
- 350
7
votes
0
answers
168
views
2022 Community Moderator Election
The 2022 Community Moderator Election is now underway!
Community moderator elections have three phases:
Nomination phase
Primary phase
Election phase
Most elections take between two and three weeks, ...
6
votes
2
answers
165
views
Why is a question about dependent type theory off topic?
The question Elimination rule for identity types in Martin-Lof Type Theory [closed] was recently closed for being off-topic.
While I agree it should have been closed for being a duplicate, I don't see ...
- 2,330
6
votes
1
answer
111
views
Not correct to say that lean community is mostly mathematicians
I noticed Guy Coder made a number of edits to a lot of tags. I accepted them all since overall they were much better, but on the same time in a number of them he suggested that lean (especially Lean ...
- 10.2k
6
votes
2
answers
68
views
Removing the [recommendations] tag
There is a recommendations tag on Proof Assistants.
Should this be deleted, as it encourages opinion-based answers?
- 1,348
6
votes
1
answer
63
views
Good "What is an X" questions & good answers to them
There are a lot of terms in the proof assistant / type theory literature that I'm either not familiar with or have an intuitive understanding of but not a definition for. I also think this type of ...
- 3,561
6
votes
0
answers
47
views
2024 Community Moderator Election Results
Proof Assistants's Moderator election #2 has come to a close. Since there were not enough candidates for a competitive election, we simply appointed the candidates who nominated themselves:
They will ...
- 101
6
votes
0
answers
41
views
Are questions about categorical logic on topic?
Are questions about categorical logic and the related category theory are on topic on this website? Categorical logic is strongly connected to type theory and the semantic of (many) proof assistants, ...
- 732
6
votes
0
answers
83
views
Should we have a Citation Helper?
It looks like a great deal of questions so far are about theoretical aspects of proof assistants and the underlying type theories. The answers to these questions rely on academic papers and conference ...
5
votes
3
answers
83
views
Can I forward questions here from other SE sites?
Questions relevant to proof assistants often get asked on other StackExchange sites. For example, the last such question I read was this. Can I import those questions to PA, both to establish whether ...
- 1,063
5
votes
1
answer
70
views
Should "Proof Assistants for Vim Users" be made community wiki?
A while ago I asked a question about information regarding vim support for various proof assistants.
As I've had answers come in, I've started wondering if we should make it community wiki, since I ...
- 329
5
votes
1
answer
32
views
Code Reviews on topic?
There are two related questions here:
Question 1: Reviewing proof scripts? I just formalized a type system in Coq (and I'm almost certain it is not "idiomatic Coq"), would it be appropriate ...
- 1,749
5
votes
0
answers
119
views
What is wrong with the question "Formalizations of unsolved problems"?
There are comments suggesting that the question Formalization of unsolved problems should be closed because it doesn't contain the big-list tag. I don't understand this. Am I missing something?
...
- 10.2k
5
votes
0
answers
106
views
Making / keeping the site expert friendly
I'm a novice at this subject. There are many questions I could ask that are pretty basic. These sorts of questions may have some benefit to future readers, since getting a critical mass of knowledge ...
- 3,561
4
votes
2
answers
113
views
How can the actual count of those eligible to vote be determined?
In the election chat room I gave a count of the number of users allowed to vote: 126 users. I did this by looking at the users page and just counting them by hand. It started a series of others ...
- 2,856
4
votes
2
answers
158
views
Can the SE staff give this site more love and attention, we are only two days old? :-)
With regards to tag edits, this has been holding me up for a few hours.
Also with the limit of 20 edits I tend to hit the limit after a few hours of editing tags.
Can the SE staff check and clear the ...
- 2,856
4
votes
2
answers
110
views
Should we allow Rosetta-Stone style questions?
This question was raised in the comments of this question about idiomatic ways to prove the associativity of append.
A Rosetta Stone style question would describe some kind of task in a prover-neutral ...
- 3,561
4
votes
1
answer
62
views
Engineerings questions on internal details of Proof Assistant implementations, usage and modifications?
I am trying to understand if PA.SE is more for maths or for programming. I have a detailed question on the internals of Coq and cannot decide if to put it here or to put it in the regular stack ...
- 383
4
votes
2
answers
54
views
How detailed should tags be?
I saw a tag coq-definition. Should there be $\forall l\in \text{ProofAssistants}, l\text{-definition}$ tag? Should there be like ...
ice1000Mod
- 6,522
4
votes
1
answer
38
views
Is it possible to transfer my questions from other SE sites? [duplicate]
I have ~20 questions on Stack Overflow about Isabelle and Coq. Most of them (probably all of them) would be better suited here, and were only posted on SO because I had no better SE site to post to.
I ...
- 101
4
votes
2
answers
51
views
What are my current privileges?
For many seasoned StackExchange users we have enough rep that we no longer check our privileges and over the years have forgotten how, count me in.
As this moves from private beta to public beta and ...
- 2,856
4
votes
1
answer
42
views
Why is this site not showing up in "More stack exchange communities"?
When I click on the little Stack Exchange icon in the upper-right corner of the viewport, it shows a list of "Your communities" and "More Stack Exchange communities".
Why does this ...
4
votes
1
answer
50
views
Where do we define and keep track of the scope of the site
I recently voted to close What is known about minimal sets of axioms?, because I think it would be better suited for (say) maths.SE.
The close vote options are:
This question does not appear to be ...
- 2,330
4
votes
1
answer
99
views
Site incorrectly shows that I have modified questions
I noticed that the PA website seems to be incorrectly reporting that somebody has modified a question. The system said I modified a question before I even made any edits. I think what probably ...
- 2,662
4
votes
1
answer
68
views
Policies on answers porting code
In questions such as this, the OP asks for proofs, definitions, methodology etc. on a specific topic, but does not require a specific proof assistant*. There will imaginably be answers that are purely ...
TreborMod
- 4,334
4
votes
1
answer
66
views
Tag for questions about definitions and approach
I asked this question about Coq recently.
I'm curious what the correct tag would be for this type of question. In the linked question, I'm asking about the possible ways of taking a pre-existing type ...
- 3,561
4
votes
0
answers
28
views
On tags for technical support
I doubt that tags like installation is of any use. No one is probably going to watch or use this tag, because people don't tend to learn everything about the installation of every proof assistant.
I ...
TreborMod
- 4,334
4
votes
0
answers
38
views
Renaming "extensional-equality" to "extensional-type-theory"
Is there any better suggestion or reasons against changing extensional-equality to extensional-type-theory? As Couchy suggests, the current tag is slightly ambiguous. If there is no objection, I think ...
TreborMod
- 4,334
4
votes
0
answers
40
views
How to write a tag wiki excerpt?
I'm hoping to establish some sort of guideline for writing tag wiki excerpts (or usage guidance).
Examples of tag wiki excerpts I find usually fall into two categories. The first references the tag ...
- 2,330
4
votes
0
answers
20
views
Tags for Isabelle Locales and Classes
I believe having a locales for Isabelle will help with organizing questions. I have added Tag info but it is still pending in peer review.
Now the main question is about this question which is ...
- 1,148
3
votes
3
answers
85
views
Now that we have our first wiki answer should all the other answers be combined into one?
This is the first question with wiki answers.
For a wiki
Voting on a community wiki post does not affect the author's reputation.
(ref)
As such there really is no need to keep all of the ...
- 2,856
3
votes
2
answers
107
views
Custom Themes and Icons
Many SE sites have custom backgrounds, badge icons and fonts. Also, would we change the PA.SE icon logo?
e.g. CS.SE, ELL.SE and Cooking.SE.
Would we get one?
- 1,348