Proof-golf is a competition to prove a particular theorem/statement using the fewest number of substitutions/steps given a set of axioms.
What is proof-golf?
proof-golf is a competition to prove a particular statement using the fewest steps.
What are the requirements of proof-golf?
There should be a complete and unambiguous set of well-defined axioms and a definition of what constitutes a single valid step in the proof. Nothing outside of what is stated in the axioms should be allowed in proofs.
Answers are scored by the number of steps of the proof as defined by the question. One step is usually considered the application of one of the axioms, and one should have good reason to define it otherwise.
Example specification
Adapted from (-a) × (-a) = a × a
Your task is to prove a + b = b + a using the group axioms plus self inversion. To avoid ambiguity here are the group axioms where + is a closed binary operation on some set S, and a, b, c are members of S:
a + (b + c) = (a + b) + c
a + 0 = a
0 + a = a
a + a = 0
Your proof should be a string of equalities each being the application of one axiom.
You may apply the axioms to either the entire expression or to some sub-expression. For example if we have (a + a) + (a + a) we can apply Axiom 4 to just the first term, just the second term or the entire expression as a whole. The variables can also stand in for arbitrarily complex expressions for instance we can apply axiom 4 to ((a + c) + b) + ((a + c) + b) to get 0. In each step of the proof you can only apply one axiom to one expression. All axioms are bidirectional, meaning substitution can go in either direction.
What makes a good proof-golf?
- Thoroughly specified.
- Simple enough to be understood in at most two quick readings of the statement and axioms.
- Complex enough to admit at least two different competitive/reasonable ways of proving the statement.
How should I answer a proof-golf? Hints?
- Use a whiteboard or a sheet of paper to draft out proof ideas first, then once you have a proof, write it up formally as an answer.
- Look at existing answers for hints on how to get between two statements.
- Avoid wasting steps expanding and then simplifying statements unless necessary for the proof.
