14
\$\begingroup\$

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.)

\$\endgroup\$
  • 1
    \$\begingroup\$ There are more moves than those: Specifically, placing an arbitrary point (for example, a point somewhere in a circle, somewhere along a line, etc). \$\endgroup\$ – Nathan Merrill Jul 24 '18 at 4:28
  • \$\begingroup\$ Not related: euclidea.xyz :) \$\endgroup\$ – user202729 Jul 24 '18 at 4:39
  • 1
    \$\begingroup\$ 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. \$\endgroup\$ – Peter Taylor Jul 24 '18 at 20:10
  • 5
    \$\begingroup\$ I think this is more aptly described by atomic-code-golf, of which I consider proof golf to be a subset. \$\endgroup\$ – xnor Jul 25 '18 at 0:20
  • 1
    \$\begingroup\$ 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 \$\endgroup\$ – Nathan Merrill Jul 25 '18 at 1:16
  • 6
    \$\begingroup\$ @NathanMerrill, there's a very big difference between axiom and operation. \$\endgroup\$ – Peter Taylor Jul 25 '18 at 6:28
  • 1
    \$\begingroup\$ @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. \$\endgroup\$ – Nathan Merrill Jul 27 '18 at 16:18
  • \$\begingroup\$ 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. \$\endgroup\$ – trichoplax Sep 30 '18 at 19:10
28
\$\begingroup\$

Yes, as long as it is well-specified

For , we validate the prove by mentally following it. For compass and straightedge, this means that a reader should be able to come out with the same solution given the same set of steps.

Furthermore, each of the possible steps should have a well-specified score (Does placing a point increase your score?)

Ideally, there would also be an interpreter we can use. Even better would be a language designed to construct compass-and-straightedge.

\$\endgroup\$
  • 1
    \$\begingroup\$ +1 for "Yes". - \$\endgroup\$ – Nathaniel Aug 1 '18 at 12:50

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .