All Questions

Filter by
Sorted by
Tagged with
0 votes
1 answer
11 views

Are software-level questions about proof assistants questions on-topic? Like how to install/run/open Coq/Lean?

It's mainly regarding this question.
ice1000's user avatar
  • 6,186
5 votes
0 answers
40 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 ...
SpencerG's user avatar
  • 101
0 votes
0 answers
35 views

2024 Community Moderator Election

The 2024 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, ...
2 votes
0 answers
34 views

Why are we having an election?

An election was just announced: Announcing a Pro Tempore election for 2024, however no explanation was given about the reason for this election. We already had an election in 2022 and we have three ...
Nike Dattani's user avatar
  • 1,165
0 votes
0 answers
41 views

Announcing a Pro Tempore election for 2024

Summary: Proof Assistants Stack Exchange will begin the nomination stage for a special election on April 9th, 2024 to bring in 2 more moderators. For full details of the process, see the announcement ...
SpencerG's user avatar
  • 101
0 votes
2 answers
28 views

Are we out of beta yet?

Can someone explain whether we are out of beta, and if we're not, what needs to happen? Or is it the case that the site banner has not been updated, but we are otherwise out of beta?
Andrej Bauer's user avatar
  • 9,154
0 votes
1 answer
30 views

Hobbled math processing on this site?

In a site about proof assistants, I'd expect to be able to format mathematics reasonably smoothly, but many things ( cases, newline, and set-brackets are just two of the things that I've found so far )...
John's user avatar
  • 367
0 votes
0 answers
41 views

What do we do about the Coq tag wrt the rename to Rocq?

Since the language Coq has been renamed to Rocq, should we also rename or redirect the tag?
ice1000's user avatar
  • 6,186
0 votes
0 answers
5 views

2023: a year in moderation

It’s that time of the year again! As we wave goodbye to last year and welcome the new one, we have a tradition of sharing moderation stats for the preceding calendar year. As most of you here might be ...
JNat's user avatar
  • 101
1 vote
0 answers
41 views

Syntax highlighting for Isabelle

I am to start a project with a student to implement syntax highlighting for Isabelle that could be used here on the Proof Assistants Stack Exchange site. Is there already some effort aiming this? ...
Gergely's user avatar
  • 311
2 votes
0 answers
30 views

Are questions about automated theorem provers on topic?

I asked the what is needed to move from design by contract to using a proof assistant? not realizing that proof assistant seems to imply interactivity. I now realize I meant something else - automated ...
Bruce Adams's user avatar
3 votes
0 answers
81 views

New SE site for Programming Language Design

As Proof Assistants is one of the newest SE sites, many of you might remember the process that's in place for getting a new site approved, and many of you might remember how exciting it is to be one ...
Nike Dattani's user avatar
  • 1,165
3 votes
0 answers
11 views

2022: a year in moderation

As we say goodbye to the old year and welcome the new one, we have a tradition of sharing moderation stats for the preceding calendar year. As most of you here are aware, sites on the Stack Exchange ...
JNat's user avatar
  • 101
4 votes
0 answers
26 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 ...
Trebor's user avatar
  • 3,967
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 ...
Charlie Parker's user avatar
0 votes
0 answers
54 views

Late Answers: How Late is Late?

In the help center, it says: The Late answers queue contains answers that were posted by new users much later than when the question was asked. What timespan is "much later"?
taylor.2317's user avatar
  • 1,318
7 votes
2 answers
135 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: ...
zacque's user avatar
  • 350
4 votes
1 answer
22 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 ...
Alex Nelson's user avatar
  • 1,564
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 ...
Trebor's user avatar
  • 3,967
6 votes
0 answers
38 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, ...
Nico's user avatar
  • 722
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 ...
Couchy's user avatar
  • 2,231
3 votes
0 answers
28 views

Should I create tags for common components in proof assistant implementations?

I'm asking questions about certain type-checking phases of a proof assistant (conversion-check, elaboration, ...
ice1000's user avatar
  • 6,186
4 votes
2 answers
53 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 ...
ice1000's user avatar
  • 6,186
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 ...
Catija's user avatar
  • 101
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. ...
Bella_Blue's user avatar
  • 101
4 votes
2 answers
112 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 ...
Guy Coder's user avatar
  • 2,846
9 votes
2 answers
185 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 ...
Eric's user avatar
  • 971
5 votes
0 answers
116 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? ...
Jason Rute's user avatar
  • 8,685
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, ...
0 votes
0 answers
27 views

Reputation Error on Main Reputation Site

When looking at PA.SE's main reputation, I can see that Namdak Tonpa's quarterly reputation is higher than the total reputation. How is this possible? Which one is erroneous?
taylor.2317's user avatar
  • 1,318
3 votes
2 answers
106 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?
taylor.2317's user avatar
  • 1,318
3 votes
0 answers
61 views

I still have access to the review queues

The site is now public but I am still seeing a link to the review queues. I also still have the close vote privilege on ProofAssistants.meta Can someone please fix? Update: It's fixed now.
Henry WH Hack v3.0's user avatar
15 votes
0 answers
249 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 ...
Catija's user avatar
  • 101
2 votes
0 answers
76 views

Is there a post that compares major proof assistants?

Is there a post that compares major Proof Assistants and provides suggestions of when to use each one, e.g. comparing: Agda, Coq, Idris, Isabelle, and Lean? With suggestions If not, can create a post?
Tim's user avatar
  • 101
2 votes
2 answers
67 views

How to get more daily views?

The weakest point on the Area 51 Site is our views. We need to get a lot more if the site wants to leave beta. But, how can we do this? As it says: Eventually, 90% of a site's traffic should come ...
taylor.2317's user avatar
  • 1,318
2 votes
1 answer
38 views

Redirected to page announcing PA private beta?

I'm unable to navigate to the main Proof Assistants site. I was clicking on an item in my reputation changes notifications, and it brought up a page announcing the beta would become public "in a ...
hardmath's user avatar
  • 539
6 votes
0 answers
79 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 ...
François G. Dorais's user avatar
2 votes
0 answers
27 views

Tags concerning variables and bindings

Should the tags bound-variables binders (and possibly de-bruijn-indexing) be merged? There probably won't be any question exclusively discussing binders and not bound variables. De bruijn indices, in ...
Trebor's user avatar
  • 3,967
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 ...
Couchy's user avatar
  • 2,231
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 ...
tinlyx's user avatar
  • 2,034
4 votes
1 answer
65 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 ...
Greg Nisbet's user avatar
  • 2,771
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 ...
Trebor's user avatar
  • 3,967
4 votes
2 answers
106 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 ...
Greg Nisbet's user avatar
  • 2,771
5 votes
0 answers
101 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 ...
Greg Nisbet's user avatar
  • 2,771
5 votes
1 answer
69 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 ...
Chris Grossack's user avatar
6 votes
1 answer
110 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 ...
Jason Rute's user avatar
  • 8,685
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 ...
Luiz Martins's user avatar
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 ...
James Wood's user avatar
  • 1,053
6 votes
1 answer
55 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 ...
Greg Nisbet's user avatar
  • 2,771
6 votes
2 answers
157 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 ...
Couchy's user avatar
  • 2,231

15 30 50 per page