Taxicab Erdős–Mordell Conjecture 1 — Proof Available

Statement

Use fixed coordinates on ℝ². For points U, V, the taxicab distance is

d(U, V) = |U_x − V_x| + |U_y − V_y|.

For distinct U, V, the taxicab distance from P to the infinite line through U and V is

h(P; U, V) = |(V_x − U_x)(P_y − U_y) − (V_y − U_y)(P_x − U_x)| / max(|V_x − U_x|, |V_y − U_y|).

Theorem. Let A, B, C satisfy det(B − A, C − A) ≠ 0. For any real α, β, γ > 0 with α + β + γ = 1, put P = αA + βB + γC. Then

2 (d(P, A) + d(P, B) + d(P, C)) ≥ 3 (h(P; B, C) + h(P; C, A) + h(P; A, B)).

That is, the sum of taxicab distances from an interior point to the vertices is at least 3/2 times the sum of its taxicab distances to the three side lines. There is no orientation restriction, and all three line-distance denominators are proved positive.

Sharpness. For every real k > 3/2 there is a nondegenerate triangle and a strictly interior point with Σd < k Σh. The example A = (−1, 0), B = (1, 0), C = (0, 1), P = (0, ε) has Σd = 3 + ε and Σh = 2 − ε for 0 < ε < 1.

What is proved

• Proved: the inequality above for every nondegenerate triangle, in every orientation, and every strictly interior point; and that the coefficient 3/2 cannot be increased.
• Distances: the distances are to the infinite supporting lines of the sides, not to the side segments.
• Why orientation matters: rotations are not symmetries of the taxicab metric, so the general orientation case does not reduce to the restricted positions treated in the original paper.
• Not new here: the constant 3/2 and the sharpness obstruction already appear in the original paper. Coordinate-median minimization and piecewise linear estimates are established methods.

Proof outline

Each side-line distance is at most the distance to either endpoint of that side, which proves the inequality on the boundary. The coordinatewise median of the three vertices lies in the closed triangle, including coordinate ties. Within the triangle, the sum of vertex distances equals its value at that median plus the distance to the median, while the sum of line distances is affine.

Interpolating between the median and the boundary therefore reduces the problem to the median. Coordinate reflections and an interchange of the axes put that case into a form handled by a piecewise affine estimate and an exact polynomial identity. The repository's readable proof gives the complete argument and the sharpness example.

Verification and trust model

The proof is formalized in Lean 4.35.0 (commit eb6cafb) with Mathlib v4.35.0 (commit 56a0058). The compiler archive is pinned by SHA-256 and every dependency revision is locked.

./verify.sh cleans and rebuilds all nine project modules, then checks Verification.lean with lake env lean --trust=0. That file independently restates the target in raw coordinates, with the determinant hypothesis and all three determinant-over-maximum line distances written out, and separately proves each denominator positive. The audit requires the printed axiom report of each of five declarations to be exactly propext, Classical.choice, and Quot.sound:

• Taxicab.taxicab_erdos_mordell_strict: the main strict-interior theorem
• TaxicabVerification.exact_statement: the raw-coordinate target
• TaxicabVerification.exact_denominators_positive: positive side denominators
• Taxicab.sharpness: every coefficient greater than 3/2 fails
• Taxicab.sharpness_distances: the exact sums in the example

Trust model: Lean's kernel and these three standard axioms. The sources contain no sorry, admit, custom axiom, or native_decide. A SHA-256 manifest covers the proof, documentation, pins, and scripts; the committed evidence records those hashes, and GitHub Actions repeats the full check on pushes and pull requests.

Prior-art search

The original paper's Theorem 2 establishes the coefficient 3/2 for restricted coordinate positions (A = (0, r), B = (p, 0), C = (q, 0), with the stated sign and ordering cases and coordinate reflections). Conjecture 1 asks for every orientation.

Earlier proof by Principia Math in Progress. A write-up for MathDB 341671, dated 12 September 2026 by its authors, presents a proof of the inequality with coefficient 3/2 for a strictly interior point of any nondegenerate triangle in every real normed plane, for distances to the side lines and to the side segments, and states that 3/2 is optimal in the taxicab plane. It was originally hosted on principia-math.com; a Lean formalization of the inequality (not of the sharpness example) was committed to PrincipiaMathOrg/math-solutions on 26 October 2026. The write-up date is author-entered and has not been independently confirmed, and neither document has been reviewed here.

The bounded, AI-assisted literature search carried out for this repository in October 2026 missed that write-up. It was found on 27 October 2026 during a search-engine and GitHub check of this page's discoverability. The repository's own prior-art notes predate that finding.

Access limitation: the full text of M. Ghandehari and H. Martini, On the Erdős–Mordell inequality for normed planes and spaces, Studia Sci. Math. Hungar. 55 (2018), 174–189 (DOI), was not accessed, so its full scope has not been checked.

Provenance

Chris Ozols, with AI-assisted proof development and formalization. Chris directed the work and its verification; OpenAI assistants contributed to the proof, the Lean formalization, and the package. Private proof development and initial Lean verification took place on October 16, 2026 (UTC). Commit dates and hashes identify content; they do not establish priority.

Sources, verification, and records

Original problem

• Petrović–Malešević–Banjac (2020), Conjecture 1, PDF page 20
• DOI 10.7153/jmi-2020-14-84
• arXiv:1901.08758

Proof and formalization

• GitHub repository
• Readable proof (PROOF.md)
• Main Lean theorem (Taxicab/Main.lean)
• Sharpness (Taxicab/Sharpness.lean)
• Exact-statement check (Verification.lean)

Verification evidence

• Verification report
• Recorded verification (verification.json)
• Full transcript (verification.log)
• Theorem types and axioms (kernel-check.log)
• Source manifest (SOURCE_SHA256SUMS)
• GitHub Actions verification runs

Prior art and provenance

• Earlier proof: Principia MathDB 341671 write-up (dated 12 September 2026)
• Prior-art review (PRIOR_ART.md)
• Discovery summary (DISCOVERY.md)
• Provenance (PROVENANCE.md)
• Citation metadata (CITATION.cff)