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.
5 questions
11
votes
0
answers
721
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,188
25
votes
2
answers
766
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 ...
- 100k
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 ...
- 100k
136
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 ...
- 100k
22
votes
3
answers
997
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
...
- 100k