[b33j0r]

QED. I’m curious now.

In your example, let’s strip each statement of phrasing (“meet at” means the same as “intersect”, etc). Also, each requires external knowledge of the relationship between radii and right angles. These bits can presumably be reduced to the same clauses as well.

So. Is more information encoded in the proof than the construction?

Is one of two equivalent prolog programs just written upside down, while the other says “hence” a non-zero number of times??

[anderskaseorg]

My example was so simple that it would be taken as obvious for an experienced reader. With any nontrivial problem, the proof would have much more information than the construction. For example, the proof might require the construction of auxiliary objects not used in the main construction.

This is beautifully showcased by a 3Blue1Brown video about an extremely clever proof of the equivalence of three constructions of an ellipse: https://www.youtube.com/watch?v=pQa_tWZmlGs.

[b33j0r]

I’m not Godel, but my ad absurdum was meant to be slightly weirder than the objection that seems to have come across. I’ll try this way.

I had a flash of a question about whether the external information required in either case offsets the information provided by the objects in the proof (implicitly, explicitly, or artificially). I was thinking in terms of both formal logic and entropy, loosely.

The (usefully simple) construction here implies use of a compass or string. In a sense, the physical constraints of a compass encode the same information as the lemmas and theorems do abstractly.

“Brah, you should google metaphysics and Bertrand Russell,” is probably about right But, I’m sure there is a term that I just don’t know or can’t recall.

[anderskaseorg]

Perhaps an answer to one version of your question is that the Tarski–Seidenberg theorem implies that Euclidean geometry is decidable: there exists an algorithm that finds a proof for any theorem of Euclidean geometry. This algorithm, however, is too slow to be practical in general (double exponential time). The proofs it finds definitely don’t correspond one-to-one with the constructions in any reasonable sense.

The compass encodes a constant-radius constraint, and the string encodes a sum-of-distances constraint, but it’s not at all obvious why these two constraints turn out to be the same under a uniform stretching. There are plenty of similar-looking hypotheses that turn out to be false (for example, a curve of constant offset to an ellipse looks a lot like an ellipse but isn’t one).