Questions tagged [proof-golf]
Proof-golf is a competition to prove a particular theorem/statement using the fewest number of substitutions/steps given a set of axioms.
7 questions
1 vote
1 answer
302 views
The Parable of the Dagger Prelude
Taken from lesswrong.com Once upon a time, there was a court jester who dabbled in logic. The jester presented the king with two boxes. Upon the first box was inscribed: "Either this box ...
- 268
7 votes
2 answers
329 views
Fitch Proof of \$(p\Longrightarrow q)\iff\lnot p\lor q\$ with least amount of steps
In the smallest amount of steps, prove $$(p\Longrightarrow q)\iff\lnot p\lor q$$ We base the proof system on this website. The related functionalities are: Assumption. Assume that some statement is ...
- 2,004
12 votes
1 answer
852 views
Lean golf: Balanced Bracket Sequence
Ungolfed, ugly, horrible proof to help you make progress on this challenge: https://gist.github.com/huynhtrankhanh/dff7036a45073735305caedc891dedf2 A bracket sequence is a string that consists of the ...
- 1,211
25 votes
2 answers
841 views
Existential Golf
Math has a lot of symbols. Some might say too many symbols. So lets do some math with pictures. Lets have a paper, which we will draw on. To start the paper is empty, we will say that is ...
- 103k
42 votes
3 answers
2k views
(A → B) → (¬B → ¬A)
Well I think it is about time we have another proof-golf question. This time we are going to prove the well known logical truth \$(A \rightarrow B) \rightarrow (\neg B \rightarrow \neg A)\$ To do ...
- 103k
137 votes
11 answers
14k views
(-a) × (-a) = a × a
We all know that \$(-a) \times (-a) = a \times a\$ (hopefully), but can you prove it? Your task is to prove this fact using the ring axioms. What are the ring axioms? The ring axioms are a list of ...
- 103k
22 votes
3 answers
1k views
Prove DeMorgan's laws
Using the the ten inferences of the Natural Deduction System prove DeMorgan's laws. The Rules of Natural Deduction Negation Introduction: {(P → Q), (P → ¬Q)} ⊢ ¬P ...
- 103k