22 votes
Accepted

Curious about computer-assisted NP-completeness proofs

As for question 2, there are at least two examples of $NP$-completeness proofs that involve computer-assistant. Erickson and Ruskey provided a computer-aided proof that Domino Tatami Covering is NP-...
21 votes
Accepted

Formalizing Homotopy Type theory in Idris

Here is a small, incomplete, and inconsistent formalization of HoTT in Idris. It shows that you can derive a contradiction in Idris just by postulating univalence. There are two barriers to ...
21 votes

What should a proof of correctness for a typechecker actually be proving?

That's a good question! It asks what we expect from types in a typed language. First note that we can type any programing language with the unitype: just pick a letter, say ...
  • 26.8k
19 votes
Accepted

Proof relevance vs. proof irrelevance

There are several possible notions of proof relevance. Let us consider three similar situations: An element of a sum $\Sigma (x : A) . P(x)$ is a pair $(a, p)$ where $a : A$ and $p$ is a proof of $P(...
  • 26.8k
15 votes
Accepted

Proof assistant usage in complexity theory research?

A general rule of thumb is that the more abstract/exotic the mathematics you want to mechanise, the easier it gets. Conversely, the more concrete/familiar the mathematics is, the harder it will be. So ...
15 votes

Curious about computer-assisted NP-completeness proofs

In this paper, I showed that if for some $k\geq 3$ there is a graph with maximum degree $k$ and chromatic edge strength strictly greater than $k$, then it is $\Theta_2^p$-complete to decide if ...
  • 1,968
14 votes

Curious about computer-assisted NP-completeness proofs

From the comment above: I used the Choco Java library for Constraint programming to check the correct behaviour of the gadgets used to prove the NP-completeness of the following puzzles: Binary ...
14 votes

Proof relevance vs. proof irrelevance

I recommend that everyone first read Andrej Bauer's answer, as he covers all the basics extremely well. I agree with everything he says in his answer. I humbly offer more comments, even though I know ...
13 votes

Humanifying computer-generated or computer assisted proofs

You are probably thinking of Gower's work with Ganesalingam, based on the latter's MSc dissertation (1). Gowers blogged about this in (2) and other places, and they've written a paper on the subject (...
11 votes
Accepted

Has a proof checker bug ever invalidated a major proof?

To my knowledge, no machine checked proof of a complex mathematical development has ever been retracted. As Andrej points out though, it occasionally happens that soundness-breaking bugs do crop up ...
  • 13.3k
11 votes

Curious about computer-assisted NP-completeness proofs

I did this very thing — computer-assisted NP-completeness proof — in my bachelor thesis! The bad part - it's in Russian and wasn't translated to English. http://is.ifmo.ru/diploma-theses/...
10 votes
Accepted

Interesting algorithms in the formalization of the Feit-Thompson theorem?

(Turning a comment into an answer, and expanding on it) From talking to someone who worked on this: no. He invented all sorts of clever refinements to many proofs, and restructured many theory ...
10 votes
Accepted

What should a proof of correctness for a typechecker actually be proving?

The question can be interpreted in two ways: Whether the implementation does implement a given typing system $T$? Whether the typing system $T$ does prevent the errors you think it should? The ...
10 votes

Formally Verified Complexity Theory

In the following paper my colleague Uli Schöpp presents a formal verification (in Coq) of a nontrivial result by Cook and Rackoff on the computational power of graph automata. https://scholar.google....
8 votes
Accepted

Is Buchberger's algorithm or Wu's method valuable theoretically when we have the Tarski–Seidenberg theorem?

For Buchberger, it depends what you want it for, but generally speaking the answer is no. First, as pointed out on the Wikipedia article, the complexity upper bound given by Tarski-Seidenberg is ...
8 votes
Accepted

Formal semantics of tactics

I'm not sure this answers your question, but the first (?) paper on the subject of tactics appears to have been Milner's The Use of Machines to Assist in Rigorous Proof.
8 votes

Formal semantics of tactics

Obviously there is an operational semantics of Ltac by Jedynak et al.
  • 1,125
8 votes
Accepted

Small kernel (i.e. proof-verifier) for Agda?

It is true that Agda currently has a much shakier foundation than say Coq or Lean. It does have an internal term syntax that could be seen as a core language (https://github.com/agda/agda/blob/master/...
  • 356
7 votes
Accepted

Structural equality of Pi Types with heterogeneous equality?

I am not aware that J or K exists for heterogeneous equality. It does not need an elimination principle, because it can be simply defined as a sigma type: ...
7 votes

Proving running time upper bounds for algorithms in dependent type theory

As usual, (a) the high-level conceptual approach is basically the same as it is on paper, but (b) mechanization makes new things reasonable to attempt. The way you do things is to define a cost ...
6 votes

Proof assistant usage in complexity theory research?

One very prominent example is of course Gonthiers Coq formalization of the 4 color theorem in Coq which uses a lot of combinatorics. My colleague Uli Schöpp used the ssreflect library developed by ...
6 votes

Formally Verified Complexity Theory

A nice example is Hugo Férée, Samuel Hym, Micaela Mayero, Jean-Yves Moyen, David Nowak: Formal proof of polynomial-time complexity with quasi-interpretations. CPP 2018: 146-157 Their abstract (my ...
  • 161
6 votes
Accepted

Why REFL rule is primitive in HOL Light?

DEDUCT_ANTISYM_RULE only applies to propositions, while REFL applies to all terms of all types. Your suggestion only shows that ...
  • 26.8k
5 votes

What should a proof of correctness for a typechecker actually be proving?

There are a few different things you could mean by "prove that my typechecker works". Which, I suppose, is part of what your question is asking ;) One half of this question is proving that your type ...
5 votes
Accepted

Representations of Planar Graphs in Coq

The obvious resource for planar graphs in Coq would be the (modern port of) the four color theorem in Coq/SSReflect, by Georges Gonthier (and others) which obviously does need to define planar graphs. ...
  • 13.3k
5 votes

Where is the quote "Informal proofs are algorithms, formal proofs are code" from?

He doesn't cite any references for it and Google doesn't return any results so I don't think he is really quoting from anywhere. The idea that a proof is a "construction" (a term in intuitionistic/...
  • 21.3k
5 votes

Has the compactness theorem for FOL been formalized in Coq/Isabelle/etc?

Compactness for FOL was done in HOL by John Harrison, and reported at TPHOLs 1998. See Formalizing basic first order model theory.
4 votes

How would I go about learning the underlying theory of the Coq proof assistant?

The current Software Foundations book does explain all this later on: https://softwarefoundations.cis.upenn.edu/lf-current/ProofObjects.html So if you're following the book, just read on :)
4 votes

Representations of Planar Graphs in Coq

I just wanted to make some additional comments not already covered by Cody's nice answer, and also address question (2). First, Gonthier goes into detail about the representation of planar maps used ...
4 votes

Proving running time upper bounds for algorithms in dependent type theory

For verified complexity analysis in other theorem proving systems, see e.g. Tobias Nipkow's paper on this subject using the Isabelle theorem prover ("Amortised Complexity Verified" at ITP 2015) which ...

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