# Is "Proof-Golf for proofs in general" on-topic?

I recently submitted a challenge proposal on the Sandbox, which is a kind of .

Here is the background section copied from the proposal:

Compass-and-straightedge construction, a.k.a. classical construction, is the construction of lengths, angles, and other geometric figures using only an idealized ruler and compass. A ruler can only be used to draw a straight line passing through two given points; a compass can only be used to draw a circle with two given points (a center, and a point on the circle).

All compass and straightedge constructions consist of repeated application of five basic constructions using the points, lines and circles that have already been constructed. These are:

• Creating the line through two existing points
• Creating the circle through one point with centre another point
• Creating the point which is the intersection of two existing, non-parallel lines
• Creating the one or two points in the intersection of a line and a circle (if they intersect)
• Creating the one or two points in the intersection of two circles (if they intersect).

In any geometric problem, we have an initial set of symbols (points and lines), an algorithm, and some results. From this perspective, geometry is equivalent to an axiomatic algebra, replacing its elements by symbols.

This is the basis of the new kind of proof-golf: classical construction golf.

I believe this follows the concept of , but I doubt if it actually fits well with PPCG.

Peter Taylor said in the comment, "proofs in logic can be argued to be as good as programs by reference to the Curry-Howard correspondence, but I don't really see extending that to proofs in general."

So here is the question:

1. Is "Proof-Golf for proofs in general" on-topic?
2. If the answer to above is "it depends", what is the condition for such a challenge to be on-topic?

(Changing to "build an automatic theorem prover" is not an option; an article mentions such a theorem prover which has thousands of lines of code.)

• There are more moves than those: Specifically, placing an arbitrary point (for example, a point somewhere in a circle, somewhere along a line, etc). Jul 24, 2018 at 4:28
• Not related: euclidea.xyz :) Jul 24, 2018 at 4:39
• On further consideration, I'm not sure the sandboxed question is "a kind of proof-golf". The answers are constructions: proving that they are correct is a separate issue which might not be required (we don't require proofs of correctness for golfed programs) and certainly need not be short. Jul 24, 2018 at 20:10
• I think this is more aptly described by atomic-code-golf, of which I consider proof golf to be a subset.
– xnor
Jul 25, 2018 at 0:20
• I disagree: I do think this is proof-golf. For example, the top question consists of applying a series of operations to reach a particular conclusion. This is identical. I agree, the two fields have tons of overlap, but that is a separate meta issue IMO Jul 25, 2018 at 1:16
• @NathanMerrill, there's a very big difference between axiom and operation. Jul 25, 2018 at 6:28
• @PeterTaylor I obviously don't see the difference. If this does become an issue, I'd definitely love to see a meta post about it. Jul 27, 2018 at 16:18
• A comment on the sandbox post asks "Do you think this would be better here or on Puzzling?". As far as I can tell, all challenge types would technically be on topic on Puzzling, but most of them are better placed here on PPCG because they suit this more specific community. To me, this seems like a topic that would be of interest to a significant subset of the PPCG community. Sep 30, 2018 at 19:10