Skip to main content
23 votes
Accepted

How hard would it be to state P vs. NP in a proof assistant?

I'm going to disagree with DW. I think that it is possible (although difficult) for a P vs. NP result to be stated in a proof assistant, and moreover, I wouldn't trust any supposed proofs unless they ...
Joey Eremondi's user avatar
12 votes
Accepted

Is Coq synthetic or analytic?

The remark is about one specific usage of Coq, namely formalization of programming language theory. Let us first make clear the distinction between synthetic and analytic: In a synthetic approach to ...
Andrej Bauer's user avatar
  • 30.4k
10 votes
Accepted

Can a type system serve as a proof assistant for foreign functions?

Long story short: no you can't. A foreign function is like a black box and the type you ascribe to it is a promise you make: in the Curry-Howard correspondence that would correspond to adding an axiom ...
gallais's user avatar
  • 573
10 votes

How hard would it be to state P vs. NP in a proof assistant?

Using proof assistants for this purpose is certainly possible in principle, but I suspect it would take more effort than most folks who write such proofs would be interested in putting in. It would ...
D.W.'s user avatar
  • 160k
9 votes

How hard would it be to state P vs. NP in a proof assistant?

I can give a direct answer to (2): $P\ne NP$ has been stated in Lean (along with the other main results of Cook's paper, where the conjecture was first described), as part of the Formal Abstracts ...
Mario Carneiro's user avatar
8 votes

Is Goedel's 1st theorem not algorithmically derivable?

Your reasoning is incorrect. It is true that your hypothetical "proof deriver" cannot derive all true statements. No proof derivation system can, and indeed, it is not even possible to express the ...
cody's user avatar
  • 8,204
8 votes
Accepted

What makes a proof assistant a proof assistant?

I would expect a proof assistant to provide: a syntax to express some mathematical statements a syntax to express a proof of one of those statements a computational process to "check" that a proof of ...
gasche's user avatar
  • 499
8 votes

How to get an element from an existential proposition in Type theory proof assistant (Lean prover)

The existential form of the axioms of set theory is convenient for the meta-theoretic explorations of set theory, such as forcing etc., where it is important to have a minimal language to worry about (...
Andrej Bauer's user avatar
  • 30.4k
8 votes

Curry-Howard isomorphism and non-constructive logic

I think people sometimes disagree on what exactly Curry-Howard is. But, one way to look at it is an exact correspondence between the syntactic rules for logic and for type theory. For the ...
Dan Doel's user avatar
  • 2,687
7 votes
Accepted

How to Efficiently Define the Natural Numbers in Type Theory

There's nothing stopping you from defining binary numbers in type theory, and this should give greater efficiency in practice. For example: https://coq.inria.fr/library/Coq.Numbers.BinNums.html ...
Joey Eremondi's user avatar
7 votes

Why cannot match $ Bool \equiv Bool $ with $ refl $ while $1 \equiv 1$ can?

From the perspective of Homotopy Type Theory (HoTT), i.e. if we have the Univalence Axiom, there are definitely values of Bool ≡ Bool that are distinct from ...
Derek Elkins left SE's user avatar
6 votes

How would one prove the pigeonhole principle with a SAT solver?

SAT solvers work in the propositional calculus, and usually accept as input a formula in conjunctive normal form. There are several different propositional variants of the pigeonhole principle; they ...
Yuval Filmus's user avatar
6 votes
Accepted

How come identity encodes absurdity

looks entirely identity function to me, which can definitely be inhabited by a closed term A proof of $\forall C : Prop, C$ is a function from an arbitrary proposition to its proof. Since a ...
Alexey Romanov's user avatar
6 votes
Accepted

What is a quotient structure?

The idea is that two expressions which are α-equivalent are not meaningfully different. λx.λy.x and λz.λy.z are technically different expressions. They are α-equivalent, though, they intuitively ...
Édouard's user avatar
  • 176
6 votes
Accepted

Agda: Which part does this type introduce universe inconsistency?

The term you're applying ¬_ to is large: it quantifies over all M : Set and therefore has type ...
gallais's user avatar
  • 573
6 votes

What are the implications of Homotopy Type Theory?

I think the best way to understand why homotopy type theory related stuff is interesting from a computer science perspective is that is a more satisfying account of extensional equality than any prior ...
Dan Doel's user avatar
  • 2,687
6 votes
Accepted

Building non-classical logics in Agda & Coq

You can define many non-classical logics in Coq (and I assume Agda too), even if they are incompatible with the logic of your proof assistant, but you need to define the concept of inference yourself. ...
Ana Borges's user avatar
5 votes
Accepted

Explanation of implication-introduction rule

Every assumption that is introduced between brackets has to be discharged at some point for the proof to be complete. Otherwise, we could prove that $A$ is true for any given $A$ as follows. ...
Mario Román's user avatar
5 votes
Accepted

Find the loop invariant of the given while loop

At the end of each iteration you have $$ \forall j: 0 \leq j < i \implies b[j] = a[j+1] $$ which you can prove by induction. Thus, when the algorithm terminates, $i$ has reached $n-1$ and you have ...
Sebastian Oberhoff's user avatar
5 votes

What is a quotient structure?

It's a term coming from abstract algebra. When you quotient a set $S$ with respect to some equivalence relation $\sim$, you are replacing the set $S$ with its equivalence classes under $\sim$. Often ...
Yuval Filmus's user avatar
5 votes

Tool for generating all the consequences of the logical theory (general logic programming framework)?

You understand incorrectly. That is not how logic programming works. The number of consequences typically grows exponentially, or is even infinite. For instance, some consequences of $\forall x \in \...
Andrej Bauer's user avatar
  • 30.4k
5 votes
Accepted

Is there a fundamental reason/limitation, such as $P \not = NP$, that prevents computers from being able to do mathematics (proofs, etc.)?

The fundamental restriction is human computer programmers' inability so far to create computers equipped with real intelligence. "Never" is a very long time, so it's hard to accept that something will ...
gnasher729's user avatar
  • 30.1k
5 votes
Accepted

Explanation of proof of why connectedness is not conjunctively local of any order $k$

The predicate $\varphi_0$ depends on at most $k$ points. There are $k+1$ middle squares. So $\varphi_0$ cannot depend on all of them. That is, there is a middle square that $\varphi_0$ does not depend ...
Yuval Filmus's user avatar
5 votes
Accepted

What does `Dv` mean in $F\star$ language?

In the theory of computation "diverge" means "does not terminate" or "runs forever". This is a computational effect (of a peculiar kind).
Andrej Bauer's user avatar
  • 30.4k
5 votes

What makes a proof assistant a proof assistant?

I would think a proof assistant is something which can represent proofs and validate the reasoning is correct. The underlying logic/type theory just determines which reasoning can be represented and ...
AlexC's user avatar
  • 51
4 votes

Is there a fundamental reason/limitation, such as $P \not = NP$, that prevents computers from being able to do mathematics (proofs, etc.)?

It depends what you mean by "doing mathematics". If you mean large scale computation, computers can easily do this, as can be seen from programs like Wolfram Alpha. Engines like these are obviously ...
Riley's user avatar
  • 280
4 votes
Accepted

Definition of InLeft and InRight

The page you reference for Coq defines inLeft and inRight as constructors of the inductive type ...
Derek Elkins left SE's user avatar
4 votes

Is it possible to implement dependent types by any object oriented language supporting inheritance and classes?

So, things like this are possible, but the usefulness varies depending on your system. First, you can absolutely model object oriented programming in a functional, formal setting. System F-sub is the ...
Joey Eremondi's user avatar
4 votes
Accepted

Why cannot match $ Bool \equiv Bool $ with $ refl $ while $1 \equiv 1$ can?

Essentially, even without K, you can match against refl, but at least one of the endpoints must be an "unconstrained" variable. Both of these type check in Agda-...
chi's user avatar
  • 14.6k
4 votes

How hard would it be to state P vs. NP in a proof assistant?

I believe your question is not that much of a proper theory question, so with your permission I'll give it a not-so-technical answer. Why are people not using proof assistants that could verify ...
einpoklum's user avatar
  • 975

Only top scored, non community-wiki answers of a minimum length are eligible