Questions tagged [formal-proof]
The formal-proof tag has no usage guidance.
9
questions
58
votes
8
answers
12k
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 ...
- 33.9k
81
votes
3
answers
5k
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 ...
- 29.2k
61
votes
9
answers
6k
views
Techniques for debugging proofs
After writing many proofs, most of which contained errors in their initial form, I have developed some simple techniques for "debugging" my proofs. Of course, a good way to detect errors in ...
53
votes
5
answers
5k
views
How much of the ATLAS of finite groups is independently checked and/or computer verified?
In a recent talk Finite groups, yesterday and today Serre made some comments about proofs that rely on the classification of finite simple groups (CFSG) and on the ATLAS of Finite Groups. Namely, he ...
- 33.9k
37
votes
1
answer
4k
views
How much mathematics has been formally verified?
That's a vague question so allow me to tighten it up a bit.
I recently noticed that there is a formal machine verified proof of the Central Limit Theorem (CLT) implemented with Isabelle. This ...
- 8,106
20
votes
1
answer
4k
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. ...
- 29.2k
16
votes
3
answers
1k
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 ...
- 7,613
14
votes
2
answers
3k
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 ...
- 24.2k
-2
votes
1
answer
188
views
Can we have consistent theories stating opposing provability statements that are non-standardly coded?
I want to coin a notion of "strong provability", to be defined as:
$S$ is strongly provable in $T$ if and only if there is a Gödel code of its proof in $T$ that is strictly smaller than any ...
- 9,256