IMO 2024 P4

Let ABC be a triangle with AB < AC < BC. Let the incentre and incircle of triangle ABC be I and \omega, respectively. Let X be the point on line BC different from C such that the line through X parallel to AC is tangent to \omega. Similarly, let Y be the point on line BC different from B such that the line through Y parallel to AB is tangent to \omega. Let AI intersect the circumcircle of triangle ABC again at P \ne A. Let K and L be the midpoints of AC and AB, respectively.

Prove that \angle KIL + \angle Y P X = 180 \degree.

AlphaGeometry Declaration Statement

General comment:

  • We will consider the orientation of the problem as in the diagram. Other orientations will be considered similarly.

  • All angle calculations are directed angles modulo \pi.

Problem formalization:

  • We add the center for each circle when it is necessary for the construction.

  • We add points of tangency when it is necessary for the construction.

  • We manually construct an approximate diagram.

Solution:

  • Just like in AlphaGeometry 1.0, all auxiliary points in the solutions below are automatically generated by a language model.

  • All angle chasing done in the proof is Gaussian elimination. d(AB) - d(CD) is the same as the directed angle from AB to CD modulo \pi.

  • We will annotate similar triangles and congruent triangles pairs manually (shown in red).

AlphaGeometry Solution (reversed proof)

Formalization:

triangle a b c; a b < a c; a c < b c; incenter i a b c; coll x b c; x != c; foot d i b c; perp x t1 t1 i; cong i t1 i d; para x t1 a c; coll y b c; y != b; perp y t2 t2 i; cong i t2 i d; para y t2 a b; circle o a b c; line_circle_intersection p a i o a; p != a; midpoint k a c; midpoint l a b; ? angeq i l i k p x p y 1 -1 1 -1 180

Auxiliary points:
Construct e = satisfying: e i b are collinear, |l e| = |l b|

Reverse proof:
93.  d(i l) - d(i k) + d(p x) - d(p y)  + 180 = 0 (by calculation)
╰-- 92. ∠b p y = ∠i k a (by similar triangles sas)
↳(similar triangles BPY and AKI, proved using 89, 90 and 91)
|   ╰-- 91. b→p→y and i→k→a are of the same clock direction. (by diagram check)
|   ╰-- 90. ∠p b y = ∠i a k (by calculation)
|   |   ╰-- 60. ∠a p o = ∠o a p (by isosceles triangle)
|   |   |   ╰-- 4. |o p| = |o a| (by assumption)
|   |   ╰-- 59. ∠c b o = ∠o c b (by isosceles triangle)
|   |   |   ╰-- 58. |o b| = |o c| (by calculation)
|   |   |       ╰-- 7. |o a| = |o c| (by assumption)
|   |   |       ╰-- 3. |o a| = |o b| (by assumption)
|   |   ╰-- 57. p a i are collinear (by assumption)
|   |   ╰-- 18. b x d y c are collinear (by merge lines)
|   |   |   ╰-- 17. y b c are collinear (by assumption)
|   |   |   ╰-- 16. b x d c are collinear (by merge lines)
|   |   |       ╰-- 15. x b c are collinear (by assumption)
|   |   |       ╰-- 14. b d c are collinear (by assumption)
|   |   ╰-- 13. ∠a c o = ∠o a c (by isosceles triangle)
|   |   |   ╰-- 12. |o c| = |o a| (by calculation)
|   |   |       ╰-- 7. |o a| = |o c| (by assumption)
|   |   ╰-- 6. ∠o b p = ∠b p o (by isosceles triangle)
|   |   |   ╰-- 5. |o b| = |o p| (by calculation)
|   |   |       ╰-- 4. |o p| = |o a| (by assumption)
|   |   |       ╰-- 3. |o a| = |o b| (by assumption)
|   |   ╰-- 1. a k c are collinear (by assumption)
|   ╰-- 89. |a k| / |a i| = |b p| / |b y| (by calculation)
|       ╰-- 88. |a c| / |a b| = |a k| / |a l| (by similar triangles aa)
↳(similar triangles AKL and ACB, proved using 74 and 87)
|       |   ╰-- 87. ∠c b a = ∠k l a (by calculation)
|       |   |   ╰-- 86. ∠l k o = ∠l a o (by inscribed angle)
|       |   |   |   ╰-- 85. l k o a are concyclic (by inscribed angle)
|       |   |   |       ╰-- 84. ∠o l a = ∠o k a (by calculation)
|       |   |   |           ╰-- 83. ∠b l o = ∠o l a (by similar triangles sss)
↳(similar triangles ALO and BLO, proved using 80, 81 and 82)
|       |   |   |           |   ╰-- 82. b→l→o and o→l→a are of the same clock direction. (by diagram check)
|       |   |   |           |   ╰-- 81. |o l| / |o b| = |o l| / |o a| (by calculation)
|       |   |   |           |   |   ╰-- 3. |o a| = |o b| (by assumption)
|       |   |   |           |   ╰-- 80. |b l| / |b o| = |a l| / |a o| (by calculation)
|       |   |   |           |       ╰-- 52. |a l| = |b l| (by assumption)
|       |   |   |           |       ╰-- 3. |o a| = |o b| (by assumption)
|       |   |   |           ╰-- 79. ∠c k o = ∠o k a (by similar triangles sss)
↳(similar triangles AKO and CKO, proved using 76, 77 and 78)
|       |   |   |           |   ╰-- 78. c→k→o and o→k→a are of the same clock direction. (by diagram check)
|       |   |   |           |   ╰-- 77. |o k| / |o c| = |o k| / |o a| (by calculation)
|       |   |   |           |   |   ╰-- 7. |o a| = |o c| (by assumption)
|       |   |   |           |   ╰-- 76. |c k| / |c o| = |a k| / |a o| (by calculation)
|       |   |   |           |       ╰-- 75. |a k| = |c k| (by assumption)
|       |   |   |           |       ╰-- 7. |o a| = |o c| (by assumption)
|       |   |   |           ╰-- 2. a l b are collinear (by assumption)
|       |   |   |           ╰-- 1. a k c are collinear (by assumption)
|       |   |   ╰-- 79. ∠c k o = ∠o k a (by similar triangles sss) see above
↳(similar triangles AKO and CKO, proved using 76, 77 and 78)
|       |   |   ╰-- 59. ∠c b o = ∠o c b (by isosceles triangle) see above
|       |   |   ╰-- 13. ∠a c o = ∠o a c (by isosceles triangle) see above
|       |   |   ╰-- 11. ∠a b o = ∠o a b (by isosceles triangle)
|       |   |   |   ╰-- 10. |o b| = |o a| (by calculation)
|       |   |   |       ╰-- 3. |o a| = |o b| (by assumption)
|       |   |   ╰-- 1. a k c are collinear (by assumption)
|       |   ╰-- 74. ∠c a b = ∠k a l (by calculation)
|       |       ╰-- 2. a l b are collinear (by assumption)
|       |       ╰-- 1. a k c are collinear (by assumption)
|       ╰-- 73. |c y| / |y i| = |c i| / |i a| (by similar triangles aa)
↳(similar triangles CYI and CIA, proved using 70 and 71)
|       |   ╰-- 71. ∠y i c = ∠i a c (by calculation)
|       |   |   ╰-- 44. ∠b c i = ∠i c a (by assumption)
|       |   |   ╰-- 32. ∠b a i = ∠i a c (by assumption)
|       |   |   ╰-- 28. ∠d y i = ∠i y t2 (by similar triangles Ssa)
↳(similar right triangles DYI and T2YI, proved using 24, 26 and 27)
|       |   |   |   ╰-- 27. d→i→y and i→t2→y are of the same clock direction. (by diagram check)
|       |   |   |   ╰-- 26. ∠y t2 i = ∠i d y (by calculation)
|       |   |   |   |   ╰-- 25. y t2 ⊥ t2 i (by assumption)
|       |   |   |   |   ╰-- 21. i d ⊥ b c (by assumption)
|       |   |   |   |   ╰-- 18. b x d y c are collinear (by merge lines) see above
|       |   |   |   ╰-- 24. |i y| / |i d| = |i y| / |i t2| (by calculation)
|       |   |   |       ╰-- 23. |i t2| = |i d| (by assumption)
|       |   |   ╰-- 22. y t2 || a b (by assumption)
|       |   |   ╰-- 18. b x d y c are collinear (by merge lines) see above
|       |   ╰-- 70. ∠y c i = ∠i c a (by calculation)
|       |       ╰-- 44. ∠b c i = ∠i c a (by assumption)
|       |       ╰-- 18. b x d y c are collinear (by merge lines) see above
|       ╰-- 72. |c y| / |c i| = |c i| / |c a| (by similar triangles aa)
↳(similar triangles CYI and CIA, proved using 70 and 71)
|       |   ╰-- 71. ∠y i c = ∠i a c (by calculation) see above
|       |   ╰-- 70. ∠y c i = ∠i c a (by calculation) see above
|       ╰-- 69. |p b| = |p c| (by isosceles triangle)
|       |   ╰-- 68. ∠c b p = ∠p c b (by calculation)
|       |       ╰-- 60. ∠a p o = ∠o a p (by isosceles triangle) see above
|       |       ╰-- 59. ∠c b o = ∠o c b (by isosceles triangle) see above
|       |       ╰-- 57. p a i are collinear (by assumption)
|       |       ╰-- 32. ∠b a i = ∠i a c (by assumption)
|       |       ╰-- 13. ∠a c o = ∠o a c (by isosceles triangle) see above
|       |       ╰-- 11. ∠a b o = ∠o a b (by isosceles triangle) see above
|       |       ╰-- 9. ∠o c p = ∠c p o (by isosceles triangle)
|       |       |   ╰-- 8. |o c| = |o p| (by calculation)
|       |       |       ╰-- 7. |o a| = |o c| (by assumption)
|       |       |       ╰-- 4. |o p| = |o a| (by assumption)
|       |       ╰-- 6. ∠o b p = ∠b p o (by isosceles triangle) see above
|       ╰-- 63. |l a| / |a e| = |p c| / |c i| (by similar triangles aa)
↳(similar triangles ALE and IPC, proved using 61 and 62)
|       |   ╰-- 62. ∠a e l = ∠p i c (by calculation)
|       |   |   ╰-- 57. p a i are collinear (by assumption)
|       |   |   ╰-- 54. ∠l a e = ∠a e l (by isosceles triangle)
|       |   |   |   ╰-- 53. |l e| = |l a| (by calculation)
|       |   |   |       ╰-- 52. |a l| = |b l| (by assumption)
|       |   |   |       ╰-- 49. |l e| = |l b| (by assumption)
|       |   |   ╰-- 51. ∠l e b = ∠e b l (by isosceles triangle)
|       |   |   |   ╰-- 50. |l b| = |l e| (by calculation)
|       |   |   |       ╰-- 49. |l e| = |l b| (by assumption)
|       |   |   ╰-- 47. e i b are collinear (by assumption)
|       |   |   ╰-- 44. ∠b c i = ∠i c a (by assumption)
|       |   |   ╰-- 32. ∠b a i = ∠i a c (by assumption)
|       |   |   ╰-- 20. ∠a b i = ∠i b c (by assumption)
|       |   |   ╰-- 2. a l b are collinear (by assumption)
|       |   ╰-- 61. ∠a l e = ∠i p c (by calculation)
|       |       ╰-- 60. ∠a p o = ∠o a p (by isosceles triangle) see above
|       |       ╰-- 59. ∠c b o = ∠o c b (by isosceles triangle) see above
|       |       ╰-- 57. p a i are collinear (by assumption)
|       |       ╰-- 51. ∠l e b = ∠e b l (by isosceles triangle) see above
|       |       ╰-- 47. e i b are collinear (by assumption)
|       |       ╰-- 20. ∠a b i = ∠i b c (by assumption)
|       |       ╰-- 11. ∠a b o = ∠o a b (by isosceles triangle) see above
|       |       ╰-- 9. ∠o c p = ∠c p o (by isosceles triangle) see above
|       |       ╰-- 2. a l b are collinear (by assumption)
|       ╰-- 56. |b a| / |a e| = |b y| / |y i| (by similar triangles aa)
↳(similar triangles ABE and YBI, proved using 48 and 55)
|           ╰-- 55. ∠a e b = ∠b i y (by calculation)
|           |   ╰-- 54. ∠l a e = ∠a e l (by isosceles triangle) see above
|           |   ╰-- 51. ∠l e b = ∠e b l (by isosceles triangle) see above
|           |   ╰-- 28. ∠d y i = ∠i y t2 (by similar triangles Ssa) see above
↳(similar right triangles DYI and T2YI, proved using 70 and 71)
|           |   ╰-- 22. y t2 || a b (by assumption)
|           |   ╰-- 20. ∠a b i = ∠i b c (by assumption)
|           |   ╰-- 18. b x d y c are collinear (by merge lines) see above
|           |   ╰-- 2. a l b are collinear (by assumption)
|           ╰-- 48. ∠a b e = ∠i b y (by calculation)
|               ╰-- 47. e i b are collinear (by assumption)
|               ╰-- 20. ∠a b i = ∠i b c (by assumption)
|               ╰-- 18. b x d y c are collinear (by merge lines) see above
╰-- 67. ∠c p x = ∠i l a (by similar triangles sas)
↳(similar triangles ALI and CPX, proved using 64, 65 and 66)
|   ╰-- 66. c→p→x and i→l→a are of the same clock direction. (by diagram check)
|   ╰-- 65. ∠p c x = ∠i a l (by calculation)
|   |   ╰-- 60. ∠a p o = ∠o a p (by isosceles triangle) see above
|   |   ╰-- 59. ∠c b o = ∠o c b (by isosceles triangle) see above
|   |   ╰-- 57. p a i are collinear (by assumption)
|   |   ╰-- 15. x b c are collinear (by assumption)
|   |   ╰-- 11. ∠a b o = ∠o a b (by isosceles triangle) see above
|   |   ╰-- 9. ∠o c p = ∠c p o (by isosceles triangle) see above
|   |   ╰-- 2. a l b are collinear (by assumption)
|   ╰-- 64. |a l| / |a i| = |c p| / |c x| (by calculation)
|       ╰-- 63. |l a| / |a e| = |p c| / |c i| (by similar triangles aa) see above
↳(similar triangles ALE and IPC, proved using 61 and 62)
|       ╰-- 56. |b a| / |a e| = |b y| / |y i| (by similar triangles aa) see above
↳(similar triangles ABE and YBI, proved using 48 and 55)
|       ╰-- 46. |c x| / |x i| = |c i| / |i d| (by similar triangles aa)
↳(similar triangles CXI and IXD, proved using 43 and 45)
|       |   ╰-- 45. ∠x i c = ∠c d i (by calculation)
|       |   |   ╰-- 44. ∠b c i = ∠i c a (by assumption)
|       |   |   ╰-- 39. ∠t1 x i = ∠i x d (by similar triangles Ssa)
↳(similar right triangles T1XI and DXI, proved using 35, 37 and 38)
|       |   |   |   ╰-- 38. i→t1→x and d→i→x are of the same clock direction. (by diagram check)
|       |   |   |   ╰-- 37. ∠x d i = ∠i t1 x (by calculation)
|       |   |   |   |   ╰-- 36. x t1 ⊥ t1 i (by assumption)
|       |   |   |   |   ╰-- 21. i d ⊥ b c (by assumption)
|       |   |   |   |   ╰-- 16. b x d c are collinear (by merge lines) see above
|       |   |   |   ╰-- 35. |i x| / |i t1| = |i x| / |i d| (by calculation)
|       |   |   |       ╰-- 34. |i t1| = |i d| (by assumption)
|       |   |   ╰-- 33. x t1 || a c (by assumption)
|       |   |   ╰-- 21. i d ⊥ b c (by assumption)
|       |   |   ╰-- 16. b x d c are collinear (by merge lines) see above
|       |   ╰-- 43. ∠x c i = ∠d c i (by calculation)
|       |       ╰-- 16. b x d c are collinear (by merge lines) see above
|       |       ╰-- 15. x b c are collinear (by assumption)
|       ╰-- 42. |b x| / |x i| = |b i| / |i a| (by similar triangles aa)
↳(similar triangles BXI and BIA, proved using 31 and 40)
|       |   ╰-- 40. ∠x i b = ∠i a b (by calculation)
|       |   |   ╰-- 39. ∠t1 x i = ∠i x d (by similar triangles Ssa) see above
↳(similar right triangles T1XI and DXI, proved using 35, 37 and 38)
|       |   |   ╰-- 33. x t1 || a c (by assumption)
|       |   |   ╰-- 32. ∠b a i = ∠i a c (by assumption)
|       |   |   ╰-- 20. ∠a b i = ∠i b c (by assumption)
|       |   |   ╰-- 16. b x d c are collinear (by merge lines) see above
|       |   ╰-- 31. ∠x b i = ∠i b a (by calculation)
|       |       ╰-- 20. ∠a b i = ∠i b c (by assumption)
|       |       ╰-- 15. x b c are collinear (by assumption)
|       ╰-- 41. |b x| / |b i| = |b i| / |b a| (by similar triangles aa)
↳(similar right triangles BXI and BIA, proved using 31 and 40)
|       |   ╰-- 40. ∠x i b = ∠i a b (by calculation) see above
|       |   ╰-- 31. ∠x b i = ∠i b a (by calculation) see above
|       ╰-- 30. |b y| / |y i| = |b i| / |i d| (by similar triangles aa)
↳(similar triangles BIY and BDI, proved using 19 and 29)
|           ╰-- 29. ∠y i b = ∠b d i (by calculation)
|           |   ╰-- 28. ∠d y i = ∠i y t2 (by similar triangles Ssa) see above
↳(similar right triangles DYI and T2YI, proved using 24, 26 and 27)
|           |   ╰-- 22. y t2 || a b (by assumption)
|           |   ╰-- 21. i d ⊥ b c (by assumption)
|           |   ╰-- 20. ∠a b i = ∠i b c (by assumption)
|           |   ╰-- 18. b x d y c are collinear (by merge lines) see above
|           |   ╰-- 16. b x d c are collinear (by merge lines) see above
|           ╰-- 19. ∠y b i = ∠d b i (by calculation)
|               ╰-- 18. b x d y c are collinear (by merge lines) see above
|               ╰-- 16. b x d c are collinear (by merge lines) see above
╰-- 13. ∠a c o = ∠o a c (by isosceles triangle) see above
╰-- 11. ∠a b o = ∠o a b (by isosceles triangle) see above
╰-- 9. ∠o c p = ∠c p o (by isosceles triangle) see above
╰-- 6. ∠o b p = ∠b p o (by isosceles triangle) see above
╰-- 2. a l b are collinear (by assumption)
╰-- 1. a k c are collinear (by assumption)
download Download the full proof

Intuitive Explanation of the Proof (Human-written)

Summary of the key steps

  • Triangle AKI is similar to triangle BPY (s-a-s)

    • ∠AIK = ∠BYP

    • ∠AKI = ∠BPY

  • Triangle ALI is similar to triangle CPX (s-a-s)

    • ∠ALI = ∠CXP

    • ∠AIL = ∠CPX

  • Triangle BXI is similar to triangle BIA (a-a)

    • BX/XI = BI/IA

  • Triangle CYI is similar to triangle CIA (a-a)

    • CY/YI = CI/IA

Intuitions behind the auxiliary construction

The problem asks the relationship between ∠KIL and ∠XPY. The former is an angle formed by a midpoint and the incenter, which usually do not go well together and cannot be computed by the angles of the main triangle ABC. Thus, this necessitates the need for auxiliary point construction. To this end, the model constructs E, which is a point on the line BI such that ∠AEB = 90\degree. In addition, this also creates pairs of similar triangles ABE and YBI, ALE and IPC. These pairs of similar triangles would create new pairs of equal angles and equal side length ratio. Thus, the point E gives purposes to the midpoint L of AB.

To complete the proof, we need to prove ∠AIK = ∠BYP and ∠AIL = ∠CPX. To this end, we need to prove that triangle AKI is similar to triangle BPY and triangle ALI is similar to triangle CPX, which is done by side length ratio chasing, which is obtained from the pairs of similar triangles above.