Skip to content

Erdős problem 898

If A,B,C∈R2A,B,C\in \mathbb{R}^2 form a triangle and PP is a point in the interior then, if NN is where the perpendicular from PP to ABAB meets the triangle, and similarly for MM and LL, PA‾+PB‾+PC‾≥2(PM‾+PN‾+PL‾). \overline{PA}+\overline{PB}+\overline{PC}\geq 2(\overline{PM}+\overline{PN}+\overline{PL}).

Sources

Browse retained paths and inspect the exact material available for this Problem.

1 retained statement2415f78e850a

Open selected source

FormalConjectures/ErdosProblems/

898.lean

Retained formal statement1 of 1

If A,B,C∈R2A,B,C\in \mathbb{R}^2 form a triangle and PP is a point in the interior then, if NN is where the perpendicular from PP to ABAB meets the triangle, and similarly for MM and LL, PA‾+PB‾+PC‾≥2(PM‾+PN‾+PL‾). \overline{PA}+\overline{PB}+\overline{PC}\geq 2(\overline{PM}+\overline{PN}+\overline{PL}).

Conjectured by Erdős in 1932 (according to [Er82e]) and proved by Mordell soon afterwards, now known as the Erdős-Mordell inequality.

FormalConjectures/ErdosProblems/898.leanErdos898.erdos_89810 linesExact file
∀ (A B C P L M N : EuclideanSpace ℝ (Fin 2)),  AffineIndependent ℝ ![A, B, C] →    P ∈ interior ((convexHull ℝ) {A, B, C}) →      N ∈ affineSpan ℝ {A, B} →        (affineSpan ℝ {P, N}).direction ⟂ (affineSpan ℝ {A, B}).direction →          M ∈ affineSpan ℝ {B, C} →            (affineSpan ℝ {P, M}).direction ⟂ (affineSpan ℝ {B, C}).direction →              L ∈ affineSpan ℝ {C, A} →                (affineSpan ℝ {P, L}).direction ⟂ (affineSpan ℝ {C, A}).direction →                  dist P A + dist P B + dist P C ≥ 2 * (dist P M + dist P N + dist P L)
SolvedProof has a holelean4external proof

The proof uses `sorry`: part of the argument is written but not proved. Lean accepts the file; it does not accept the theorem.

Search problems.science

Find a Problem, Result, source, or page