A mathematical proof is any mathematical argument which demonstrates the truth of a mathematical statement. Informal proofs are typically rendered in natural language and are held true by consensus; formal proofs are typically rendered symbolically and can be checked mechanically. "Proofs" can be valid or invalid; only the former kind constitutes actual proof, whereas the latter kind usually refers to a flawed attempt at proof.
Questions tagged [proof]
828 questions
87
votes
9 answers
What is the Pumping Lemma in Layman's terms?
I saw this question, and was curious as to what the pumping lemma was (Wikipedia didn't help much).
I understand that it's basically a theoretical proof that must be true in order for a language to be in a certain class, but beyond that I don't…
shsteimer
- 28,436
- 30
- 79
- 95
87
votes
5 answers
Concrete example showing that monads are not closed under composition (with proof)?
It is well-known that applicative functors are closed under composition but monads are not. However, I have been having trouble finding a concrete counterexample showing that monads do not always compose.
This answer gives [String -> a] as an…
Brent Yorgey
- 2,043
- 16
- 17
85
votes
1 answer
How to read this GHC Core "proof"?
I wrote this small bit of Haskell to figure out how GHC proves that for natural numbers, you can only halve the even ones:
{-# LANGUAGE DataKinds, GADTs, KindSignatures, TypeFamilies #-}
module Nat where
data Nat = Z | S Nat
data Parity = Even |…
Mathijs Kwik
- 1,227
- 9
- 12
67
votes
7 answers
Explain the proof by Vinay Deolalikar that P != NP
Recently there has been a paper floating around by Vinay Deolalikar at HP Labs which claims to have proved that P != NP.
Could someone explain how this proof works for us less mathematically inclined people?
Nixuz
- 3,439
- 4
- 39
- 44
61
votes
31 answers
Why can't programs be proven?
Why can't a computer program be proven just as a mathematical statement can? A mathematical proof is built up on other proofs, which are built up from yet more proofs and on down to axioms - those truths truths we hold as self evident.
Computer…
4thSpace
- 43,672
- 97
- 296
- 475
37
votes
1 answer
What is Haskell missing for totality checking?
A total (functional) language is one in which everything can be shown to terminate. Obviously, there are lots of places where I don't want this - throwing exceptions is sometimes handy, a web-server isn't supposed to terminate, etc. But sometimes, I…
Alec
- 31,829
- 7
- 67
- 114
32
votes
9 answers
What is the proof of of (N–1) + (N–2) + (N–3) + ... + 1= N*(N–1)/2
I got this formula from a data structure book in the bubble sort algorithm.
I know that we are (n-1) * (n times), but why the division by 2?
Can anyone please explain this to me or give the detailed proof for it.
Thank you
skystar7
- 4,419
- 11
- 38
- 41
31
votes
1 answer
LaTeX natural deduction proofs using Haskell
How can one create LaTeX source for natural deduction proof trees (like those shown here) via Haskell eg using HaTeX? I'd like to emulate LaTeX .stys like bussproofs.sty or proof.sty.
pravnar
- 833
- 7
- 11
30
votes
1 answer
Proof that the halting problem is NP-hard?
In this answer to a question about the definitions of NP, NP-hard, and NP-complete, Jason makes the claim that
The halting problem is the classic NP-hard problem. This is the problem that given a program P and input I, will it halt? This is a…
templatetypedef
- 362,284
- 104
- 897
- 1,065
22
votes
5 answers
proofs about regular expressions
Does anyone know any examples of the following?
Proof developments about regular expressions (possibly extended with backreferences) in proof assistants (such as Coq).
Programs in dependently-typed languages (such as Agda) about regular…
user108761
22
votes
2 answers
C# Code Contracts: What can be statically proven and what can't?
I might say I'm getting quite familiar with Code Contracts: I've read and understood most of the user manual and have been using them for quite a while now, but I still have questions. When I search SO for 'code contracts unproven' there are quite a…
JBSnorro
- 6,048
- 3
- 41
- 62
21
votes
4 answers
Functional proofs (Haskell)
I failed at reading RWH; and not one to quit, I ordered Haskell: The Craft of Functional Programming. Now I'm curious about these functional proofs on page 146. Specifically I'm trying to prove 8.5.1 sum (reverse xs) = sum xs. I can do some of the…
Evan Carroll
- 78,363
- 46
- 261
- 468
18
votes
7 answers
How do you "get it" when it comes to proofs?
When we start getting into algorithm design and more discrete computer science topics, we end up having to prove things all of the time. Every time I've seen somebody ask how to become really good at proofs, the common (and possibly lazy) answer is…
Chris
- 21,549
- 25
- 71
- 99
17
votes
1 answer
Are there any Bitwise Operator Laws?
Thinking in terms of Algebraic laws, I was wondering if there are any official guide lines which exist in the realm of bit manipulations, similar to Algebra.
Algebraic Example
a - b =/= b - a
Let a = 7 and b = 5
a - b = 2
b - a = -2
Let a = 10 and…
zeboidlund
- 9,731
- 31
- 118
- 180
16
votes
1 answer
Open Type Level Proofs in Haskell/Idris
In Idris/Haskell, one can prove properties of data by annotating the types and using GADT constructors, such as with Vect, however, this requires hardcoding the property into the type (e.g. a Vect has to be a separate type from a List).
Is it…
David Harrison
- 327
- 2
- 7