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 proof-golf, 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:
- Is "Proof-Golf for proofs in general" on-topic?
- 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.)