---

Claim. For a triangle $ABC$ in the plane, a point $P$ in its interior, and the feet $L$, $M$, $N$ of the perpendiculars from $P$ to the three sides,

$$\overline{PA} + \overline{PB} + \overline{PC} \ge 2\,(\overline{PL} + \overline{PM} + \overline{PN}).$$

This is the statement of Problem 898, now called the Erdős–Mordell inequality. Erdős posed it as Problem 3740 of the American Mathematical Monthly in 1935; Mordell proved it, and simpler proofs followed (Kazarinoff 1957, Bankoff 1958).

Source. The first publication of Mordell's proof is L. J. Mordell, Középiskolai Matematikai Lapok 11 (1935), 146–148, cited so by Erdős's survey of 1982 (card, section I.1, p. 61, the site's reference [Er82e]), which dates the conjecture to 1932 and the proof to 1934 and refers to the Monthly for the proof as well; that paper is not held here and carries no record with a day, so the page is dated to its year. The second source, the paper link, is the published solution to Erdős's problem: L. J. Mordell and D. F. Barrow, Solution to Problem 3740, Amer. Math. Monthly 44 (1937), no. 4, 252–254, the problem being P. Erdős, Problem 3740, Amer. Math. Monthly 42 (1935), no. 6, 396. The page is named by Mordell alone, whom the site credits; Barrow is a co-solver of the Monthly item.

Acceptance. The Monthly solution is a refereed journal publication, the refereed evidence. The site's curator, T. F. Bloom, marks the problem proved and credits Mordell on the problem's page at erdosproblems.com (page last edited 2026-01-28); that credit is the reviewed evidence. A Lean formalization posted to the site's forum on 2026-01-28, whose author writes that he had the systems Gemini 3 Flash and Aristotle formalize a solution to the problem, and its copy in a public repository of Lean proofs of Erdős problems (the formalization link) are the site's Lean qualifier. The copy's header declares the file a formalization of a solution to the problem and lists Louis J. Mordell, Gemini 3.0 Flash and Aristotle as its informal authors and Gemini 3.0 Flash, Aristotle and JoshuaB as its formal authors; since the header names Mordell as an informal author, the file is taken as a formalization of his proof and kept as a link here rather than given a page of its own as an independent proof. This corpus has built neither file, so the claim is not formalized.