Tool for Euclidean geometry aware of logic | Hacker News Reader

Tool for Euclidean geometry aware of logic

github.com

50 pointsnotpushkin11 comments

This seems a lot like the great game Euclidea https://www.euclidea.xyz/ where you have to build target constructions in minimal steps. I highly recommend it for getting your proof fix on-the-go in your pocket when you may not have your favorite proof environment to hand. Happy proving!

Euclidea doesn’t have proofs. This does.

Constructions are implicitly proofs, aren’t they? But yes.

No. A construction says what to draw; a proof says why you’ve drawn the right thing.

Say we want to find the midpoint M of AB. Construction:

“Draw the circle centered at A through B and the circle centered at B through A. Let the two circles meet at C, D. Let AB meet CD at M.”

Proof:

“Since AC = AB = BC, C lies on the perpendicular bisector of AB. Since AD = AB = BD, D lies on it as well. Hence CD is the perpendicular bisector of AB. That means AM = BM, so M is the midpoint of AB.”

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??

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.

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.

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

In Euclidea, you don’t manipulate the proofs but unless you’re just brute-forcing the levels you have constructed a proof mentally. Similarly, if Euclidea is implemented correctly, it generates the proof internally and checks it (even if these stages are fused). I wouldn’t rely on a game for building large developments and indeed Euclidea lacks abstraction and modularity as far as I can tell but the same developer may have a freeform environment with these features. Euclidea is an activity that mentally scratches the same itch as proving and in the same or very similar theory to TFA.

This is so fun! Is the Rhombus in Rect puzzle broken? I've seem to have met all of the qualifications for it, but it's not letting me pass.

Works for me. (In case it helps, remember that a rhombus must have four equal sides, not just two pairs of equal sides.)

Reply on news.ycombinator.com