The formal-proof tag has no wiki summary.

**0**

votes

**0**answers

13 views

### Pierce's Law in HOL Light [migrated]

Im fairly new to HOL light and ocaml. Could someone please explain to me how Pierce's Law can be written in HOL Light. Thanks in advance.

**48**

votes

**3**answers

2k views

### How do I verify the Coq proof of Feit-Thompson?

I probably don't have the appropriate background to even ask this question. I know next to nothing about formal or computer-aided proof, and very little even about group theory. And this question is ...

**10**

votes

**1**answer

531 views

### Where can I find Gonthier's Coq code proving the four color theorem?

In a 2008 article in the Notices, Georges Gonthier announced a computer-checked proof of the four color theorem using Coq:
Gonthier, Georges. Formal proofâ€”the four-color theorem.
Notices Amer. ...

**0**

votes

**1**answer

658 views

### Is there any danger far from home? (Edited & Revised Version) [closed]

The notion of formal proof is defined by finite sequences ($<\omega$ - sequences) of sentences. In some sense if a sentence $\sigma$ is (finitely) provable from the theory $T$ it is very "near" to ...

**2**

votes

**1**answer

171 views

### Proof of regularity for bounded elliptic problem

We consider the boundary value problem for potential in the form:
$$-\Delta u(\boldsymbol{x})=0,\quad \boldsymbol{x}\in \mathbb R^3\smallsetminus S,$$
with boundary conditions
$$\nabla ...

**2**

votes

**1**answer

437 views

### Hilbert style axiomatic proof or sequent Calculus?

I am puzzling with the question which of the two proof systems (Hilbert style axiomatic proofs or substructural Sequent Calculi) is the most discriminatory?
With discriminatory I mean is which proof ...

**2**

votes

**1**answer

936 views

### Where is a proof of “2 is more than 1 plus 1” said by Saunders Mac Lane? [closed]

I came across this statement in the autobiography by Saunders Mac Lane.
It was the interaction between solenoids and group extension that got our collaboration started, and this first work of ...

**1**

vote

**1**answer

342 views

### Since an inconsistent system can prove its own consistency…

Say a proof for the consistency of a formal system (proved within the formal system) is known. There are two possible cases: 1. the formal system is consistent and it can be and has been proven to be, ...

**2**

votes

**1**answer

290 views

### Sequent calculus: is there a complete linear reasoning (i.e., no trees)?

In Gentzen's sequent calculus, a formal proof is described by a tree, with each node representing the sequent obtained from the child(ren) by applying a given inference rule.
If no inference rule has ...

**15**

votes

**3**answers

788 views

### Finite versions of Godel' s incompleteness

Assume you have some notion of proof complexity: for instance, at the basic level, the length of a proof, or the number of symbols used, take your pick (there are more involved measures, but for sake ...

**8**

votes

**1**answer

390 views

### Proving that a combinatorial sequence has no compact formula

Suppose we have a sequence $a_n$ given by some combinatorial formula, e.g. involving a sum of n terms (like ${n \choose k}^{10}3^{-k}$ etc.). Sometimes it is plausible that there is no compact ...

**10**

votes

**2**answers

2k views

### Consequences of technically proving anything in Coq (on at least Linux) exploiting a bug? [closed]

Technically, it is possible to prove anything in Coq proof assistant [1] (on at least Linux) due to a programming feature (or bug). This seems tractable when validating large proofs. Human analysis ...

**15**

votes

**4**answers

3k views

### How true are theorems proved by Coq?

Less tongue in cheek, is it known what the relative consistency is for theorems proved with an automatic theorem prover? Of course this depends somewhat on what assumptions one makes with respect to ...