Compfiles/Imo2025P2.lean

GitHub source file

1 declarations, 1 contain sorry, 0 declared as axioms

International Mathematical Olympiad 2025, Problem 2

Let Ω and Γ be circles with centres M and N, respectively, such that the radius of Ω is less than the radius of Γ. Suppose Ω and Γ intersect at two distinct points A and B. Line MN intersects Ω at C and Γ at D, so that C, M, N, D lie on MN in that order. Let P be the circumcentre of triangle ACD. Line AP meets Ω again at E ≠ A and meets Γ again at F ≠ A. Let H be the orthocentre of triangle PMN.

Prove that the line through H parallel to AP is tangent to the circumcircle of triangle BEF.

Imports (2)
Imported by 1 file
  1. problem Imo2025P2.imo2025_p2 sorry line 42 source

    depends on sorry what this means

    Statement uses: NormedAddCommGroup, InnerProductSpace, Real, MetricSpace, NormedAddTorsor, Fact, Eq, Nat, Module.finrank, OfNat.ofNat, EuclideanGeometry.Sphere, EuclideanGeometry.Sphere.center, LT.lt, EuclideanGeometry.Sphere.radius, Membership.mem, Set, Inter.inter, Metric.sphere, Ne, AffineSubspace and 19 more

    Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous

    40 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

    Open to load the checked before-and-after goal states.