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 fromAB
toCD
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 (Humanwritten)
Summary of the key steps

Triangle
AKI
is similar to triangleBPY
(sas)
∠AIK = ∠BYP

∠AKI = ∠BPY


Triangle
ALI
is similar to triangleCPX
(sas)
∠ALI = ∠CXP

∠AIL = ∠CPX


Triangle
BXI
is similar to triangleBIA
(aa)
BX/XI = BI/IA


Triangle
CYI
is similar to triangleCIA
(aa)
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.