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}).

No current result

No reviewed Result is current in Vela Mathematics Program. Retained source material is shown below.

Retained declaration

FormalConjectures/ErdosProblems/898.lean

Formal Conjectures

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.

Proof manifests naming this Problem

  • Jayyhk Erdős Leanjayyhk:erdos:898
  • PLBY Lean proofsErdosProblems.Erdos898

Reported activity

Work these sources record against this Problem. Source-reported attribution, not reviewed here.

  • Formalization

    Erdős AI contributions wiki · 28 Jan, 2026

    Machine
    Aristotle, Gemini 3 Flash
    Open the source record

Continue

Start a contributionBrowse the source filesOpen the collection entry

Search problems.science

Find a Problem, Result, source, or page