Skip to main content

mastodon - Link to source

On my quasi-blog:

"Brute-forcing Langley’s geometry problem with field extensions"
chiark.greenend.org.uk/~sgtath…

I ran into this geometry problem recently and decided I'd rather bludgeon it to death with algebraic number fields than look for the clever construction. Then I thought I'd write up the bludgeoning procedure.

Brute-forcing Langley’s geometry problem with field extensions

www.chiark.greenend.org.uk
in reply to Simon Tatham

Jean Abou Samra
mastodon - Link to source
Jean Abou Samra
• •
Being a computer scientist, I'd brute force it in a different way. First, guess the angle is 60° by numerical approximation. Then, encode the statement that the solution is 60° into the first-order theory of the reals (with 0, 1, +, ×) and run the decision procedure from the Tarski-Seidenberg theorem to certify it.
in reply to Simon Tatham

Alexandra Lanes
friendica (DFRN) - Link to source
Alexandra Lanes
•
@Simon Tatham When I brought that problem to you I didn’t expect it to consume the attention of three maths graduates, let alone to provoke blogging!
@Simon Tatham
in reply to Alexandra Lanes

Simon Tatham
mastodon - Link to source
Simon Tatham
• •
@ajlanes also I should point out that the version you showed me is one of the variations, with different angles from the one on Wikipedia. The same technique works fine for your variant, but I've evilly left adjusting the calculation as an exercise 😀
@Alexandra Lanes
in reply to Simon Tatham

Andrew Stacey (he/him)
mastodon - Link to source
Andrew Stacey (he/him)
• •

commenting mainly so I can find this again, but also to link to my own attempts at this problem which might be of interest as I also took a bit of an inelegant route.

loopspace.mathforge.org/Counti…

Solving a Puzzle, Mathematically

MathForge
in reply to Andrew Stacey (he/him)

Simon Tatham
mastodon - Link to source
Simon Tatham
• •

@loopspace your derivation in §5 makes me think I might have been hasty in my final "have I cheated?" section.

I claimed I had kept to the letter of the "no trigonometry" rule because I didn't _calculate_ a sine, cosine or tangent. But your §5 working shows that that's a hasty claim: there's more than one way to _use_ trigonometry in a proof. Writing down equations in the sine rule and manipulating them with trig identities is still reasoning _based on_ trigonometry, even if it never numerically calculates a value of any trig function, and would surely be rejected by someone enforcing the official rules of the puzzle. (Though, as you say, one isn't _required_ to care about that.)

So now I'm not sure whether I kept to the letter or not! Probably all the identities you can show by reducing via the minimal polynomial of t are also things you can show using trig identities and algebra. So perhaps I did use trig after all, I just disguised it better. 😀

@Andrew Stacey (he/him)
⇧