Timeline for Automatically solving olympiad geometry problems
Current License: CC BY-SA 4.0
13 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Jan 21 at 0:26 | comment | added | JoshuaZ | @KevinBuzzard , Possibly if one is continuing in the same direction, maybe going with Brahmagupta's formula's next would make sense. | |
| Aug 8, 2019 at 12:15 | comment | added | Andrea Ferretti | Another easy one is Apollonius theorem: let ABC be a triangle right in A. The midpoints of the three sides and the foot of the altitude drawn from A to BC all lie on one circle. But again, it may be too easy... | |
| Aug 7, 2019 at 18:03 | comment | added | Kevin Buzzard | We need a better toy example. | |
| Aug 7, 2019 at 12:51 | comment | added | user44143 | For what it’s worth, this can also be done easily enough by hand. We have $2ax=a^2+b^2-c^2$, so $(2ab)^2=(2ax)^2+(2ay)^2=(a^2+b^2-c^2)^2+16s^2$, and the result follows by rearranging and factoring the differences of squares. | |
| Aug 7, 2019 at 12:26 | comment | added | François Brunault | I regularly ask the students to prove Héron's formula with Sage and it works well, resultants are sufficient. | |
| Aug 7, 2019 at 12:26 | comment | added | Andrea Ferretti | @KevinBuzzard done, see my edit - in fact it was quicker and easier than I thought | |
| Aug 7, 2019 at 12:26 | history | edited | Andrea Ferretti | CC BY-SA 4.0 |
added 600 characters in body
|
| Aug 7, 2019 at 12:17 | history | edited | Andrea Ferretti | CC BY-SA 4.0 |
edited body
|
| Aug 7, 2019 at 12:06 | comment | added | Andrea Ferretti | It is a classic example, so I did not perform the computation myself, but I may try later using github.com/PoslavskySV/rings . I will let you know how long it takes | |
| Aug 7, 2019 at 11:34 | comment | added | Kevin Buzzard | I have a gut feeling that some olympiad problems will not be solvable in this way because they might involve assertions about only some roots. (a+b-c)(c+a-b)(b+c-a)(a+b+c) is a polynomial function of a^2, b^2 and c^2, so issues of sign do not show up. What about an analogous question where it's essential that b is chosen to be the positive square root, and where the claimed equation does not hold if the negative one is chosen? I think that's why Groebner bases are not sufficient here but I do not know a good toy example. | |
| Aug 7, 2019 at 11:30 | comment | added | Kevin Buzzard | Did you do these calculations? Using which system? How long did they take? | |
| Aug 7, 2019 at 10:59 | comment | added | Turbo | Looks like there should be lot more identities. | |
| Aug 7, 2019 at 9:01 | history | answered | Andrea Ferretti | CC BY-SA 4.0 |