# Tag Info

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 ...
• 29.4k
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 ...
• 28.9k
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 ...
• 563

### 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 ...
• 149k
Accepted

### Given the "programs as proofs" isomorphism, how do we know that the program isn't lying?

Proving the correctness of a program in a form of a proof that's nothing but the program itself This is not quite how the Curry-Howard-Correspondence works. First one has to show that the language ...
• 404

### 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 ...

### Can we prove that $1 + 2 + \dots + n = \frac{n(n+1)}{2}$ using a computer program?

In order with the explicit questions: Yes Yes No To answer the question I think you're attempting to ask, we can prove many things using type checking, but not everything. What does this have to do ...
• 17.9k

### 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 ...
• 7,844
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 ...
• 499

### 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 (...
• 28.9k
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 ...
• 29.4k

### 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 ...
• 11.9k
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 ...
• 563
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 ...
• 3,127

### 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 ...
• 273k

### Can we prove mathematical induction statements in Lisp?

Let me try to clarify a point that seems to be confusing you: you seem to be conflating 2 related, but different concepts. The first is the concept of a proof system, which allows you to specify and ...
• 7,844
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. ...
• 176
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 ...
• 26.8k

### Given the "programs as proofs" isomorphism, how do we know that the program isn't lying?

In some sense it doesn't matter what the function does, as long as it takes the correct types and produces something of the correct type. The trick is that when you start talking about the Curry-...
• 17.9k
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 ...
• 166

### 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 ...
• 273k