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\$
8
  • 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, 2018 at 4:28
  • \$\begingroup\$ Not related: euclidea.xyz :) \$\endgroup\$
    – DELETE_ME
    Jul 24, 2018 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, 2018 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, 2018 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, 2018 at 1:16
  • 6
    \$\begingroup\$ @NathanMerrill, there's a very big difference between axiom and operation. \$\endgroup\$
    – Peter Taylor
    Jul 25, 2018 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, 2018 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 is on Codidact now
    Sep 30, 2018 at 19:10

1 Answer 1

Reset to default
31
\$\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
  • 1
    \$\begingroup\$ +1 for "Yes". - \$\endgroup\$
    – N. Virgo
    Aug 1, 2018 at 12:50

You must log in to answer this question.

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